harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem mul_aux_left (x1 x2 y : ℕ × K) (H : R K p x1 x2) :
    mk K p (x1.1 + y.1, (frobenius K p)^[y.1] x1.2 * (frobenius K p)^[x1.1] y.2) =
      mk K p (x2.1 + y.1, (frobenius K p)^[y.1] x2.2 * (frobenius K p)^[x2.1] y.2) :=
  match x1, x2, H with
  | _, _, R.intro n x =>
    Quot.sound <| by
      rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul,
        Nat.succ_add]
      apply R.intro

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 * (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul,
  Nat.succ_add]

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x * (⇑(frobenius K p))^[n] y.2))

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x * (⇑(frobenius K p))^[n] y.2))

Tactic:
apply R.intro

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc]
lemma mapMap_D₁ (i₁₂ i₁₂' : I₁₂) :
    GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂' =
      K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂'

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂' =
    K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
    ~~~((~~~x).sshiftRight n) = x.sshiftRight n

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ ~~~(~~~x).sshiftRight n = x.sshiftRight n

Tactic:
simp [not_sshiftRight]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
/-- `starMap` is functorial:
`starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)`. -/
@[simp]
lemma starMap_id : starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)

Proof state:
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
⊢ starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)

Tactic:
ext

Result:
case h.h.h1
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).fst =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).fst

case h.h.h2
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd

Proof state:
case h.h.h1
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).fst =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).fst

case h.h.h2
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd

Tactic:
all_goals simp

Result:
no goals

Proof state:
case h.h.h2
R : Type u_1
B : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
x✝ : B
⊢ (((↑(starMap (NonUnitalStarAlgHom.id R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd =
    (((↑(StarAlgHom.id R (Unitization R B))).comp (inrNonUnitalStarAlgHom R B)) x✝).snd

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem card_ring : card Language.ring = 5

Proof state:
this : Fintype.card ring.Symbols = 5
⊢ ring.card = 5

Tactic:
simp [Language.card, this]

Result:
no goals

Proof state:
⊢ ring.card = 5

Tactic:
have : Fintype.card Language.ring.Symbols = 5 := rfl

Result:
this : Fintype.card ring.Symbols = 5
⊢ ring.card = 5
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem mapIso_inv_app (f g : X ⟶ Y) (h : f = g) (U : Opens Y) :
    (mapIso f g h).inv.app U = eqToHom (by rw [h]) :=
  rfl

Proof state:
X Y Z : TopCat
U✝ V W : Opens ↑X
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map g).obj U = (map f).obj U

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
/-- Note that most of the lemmas about powers of two refer to it as `sq`. -/
@[to_additive two_nsmul] lemma pow_two (a : M) : a ^ 2 = a * a

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 = a * a

Tactic:
rw [pow_succ, pow_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_dblU (P : Fin 3 → A) : (W'.baseChange B).toJacobian.dblU (f ∘ P) =
    f ((W'.baseChange A).toJacobian.dblU P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.dblU (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblU P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
lemma dvd_comp_X_sub_C_iff (p q : R[X]) (a : R) :
    p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
let _ := invertibleOne (α := R)

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
simpa using dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).get? k = none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).get? k = none

Tactic:
simp_to_raw using Raw₀.get?_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Tendsto.const_div {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞}
    (hm : Tendsto m f (𝓝 b)) (hb : b ≠ ∞ ∨ a ≠ ∞) : Tendsto (fun b => a / m b) f (𝓝 (a / b))

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ Tendsto (fun b => a / m b) f (𝓝 (a / b))

Tactic:
apply Tendsto.const_mul (ENNReal.tendsto_inv_iff.2 hm)

Result:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ b⁻¹ ≠ 0 ∨ a ≠ ⊤

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ b⁻¹ ≠ 0 ∨ a ≠ ⊤

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
lemma coprime_div_gcd_of_squarefree (hm : Squarefree m) (hn : n ≠ 0) : Coprime (m / gcd m n) n

Proof state:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).Coprime n

Tactic:
have : Coprime (m / gcd m n) (gcd m n) :=
  coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]

Result:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
this : (m / m.gcd n).Coprime (m.gcd n)
⊢ (m / m.gcd n).Coprime n

Proof state:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ Squarefree (m / m.gcd n * m.gcd n)

Tactic:
simpa [Nat.div_mul_cancel, gcd_dvd_left]

Result:
no goals

Proof state:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
this : (m / m.gcd n).Coprime (m.gcd n)
⊢ (m / m.gcd n).Coprime n

Tactic:
simpa [Nat.div_mul_cancel, gcd_dvd_right] using
  (coprime_div_gcd_div_gcd (m := m) (gcd_ne_zero_right hn).bot_lt).mul_right this

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.isBasis_of_closure_eq_closure (hI : M.IsBasis I X) (hY : I ⊆ Y)
    (h : M.closure X = M.closure Y) (hYE : Y ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.closure I

Tactic:
rw [hI.closure_eq_closure, h]

Result:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.closure Y

Proof state:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ M.IsBasis I Y

Tactic:
refine hI.indep.isBasis_of_subset_of_subset_closure hY ?_

Result:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.closure I

Proof state:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ Y ⊆ M.closure Y

Tactic:
exact M.subset_closure Y

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd'_eq (a b c : ℤ) (h : a + b = c) :
    CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h =
      shiftFunctorAdd' C a b c h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h = shiftFunctorAdd' C a b c h

Tactic:
ext

Result:
case w.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b c : ℤ
h : a + b = c
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h).hom.app x✝).f i✝ =
    ((shiftFunctorAdd' C a b c h).hom.app x✝).f i✝

Proof state:
case w.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b c : ℤ
h : a + b = c
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h).hom.app x✝).f i✝ =
    ((shiftFunctorAdd' C a b c h).hom.app x✝).f i✝

Tactic:
simp only [shiftFunctorAdd'_hom_app_f', XIsoOfEq, eqToIso.hom, shiftFunctorAdd'_hom_app_f]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_zero_succ (k : ℕ) : multichoose (0 : R) (k + 1) = 0

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
  factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
  smeval_X_mul, zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
    (h₂ : toInsert.contains k = false) : containsKey k (insertListIfNewUnit l toInsert) →
    containsKey k l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
⊢ containsKey k (insertListIfNewUnit l toInsert) = true → containsKey k l = true

Tactic:
intro h₁

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : containsKey k (insertListIfNewUnit l toInsert) = true
⊢ containsKey k l = true

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : containsKey k l = true
⊢ containsKey k l = true

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : (containsKey k l || false) = true
⊢ containsKey k l = true

Tactic:
simp at h₁

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : containsKey k l = true
⊢ containsKey k l = true

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : containsKey k (insertListIfNewUnit l toInsert) = true
⊢ containsKey k l = true

Tactic:
rw [containsKey_insertListIfNewUnit, h₂] at h₁

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h₂ : toInsert.contains k = false
h₁ : (containsKey k l || false) = true
⊢ containsKey k l = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_of_ne_of_mem {a y : α} {l : Vector α n} (h₁ : a ≠ y) (h₂ : a ∈ l.push y) : a ∈ l

Proof state:
α : Type u_1
n : Nat
a y : α
l : Vector α n
h₁ : a ≠ y
h₂ : a ∈ l.push y
⊢ a ∈ l

Tactic:
simpa [h₁] using h₂

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
@[simp, norm_cast]
lemma coe_valMinAbs : ∀ {n : ℕ} (x : ZMod n), (x.valMinAbs : ZMod n) = x
  | 0, _ => Int.cast_id
  | k@(n + 1), x => by
    rw [valMinAbs_def_pos]
    split_ifs
    · rw [Int.cast_natCast, natCast_zmod_val]
    · rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]

Proof state:
case pos
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑x.val = x

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

Result:
no goals

Proof state:
case neg
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑x.val - ↑(namedPattern k (n + 1) h✝¹)) = x

Tactic:
rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
  sub_zero]

Result:
no goals

Proof state:
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if x.val ≤ namedPattern k (n + 1) h✝ / 2 then ↑x.val else ↑x.val - ↑(namedPattern k (n + 1) h✝)) = x

Tactic:
split_ifs

Result:
case pos
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑x.val = x

case neg
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑x.val - ↑(namedPattern k (n + 1) h✝¹)) = x

Proof state:
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑x.valMinAbs = x

Tactic:
rw [valMinAbs_def_pos]

Result:
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if x.val ≤ namedPattern k (n + 1) h✝ / 2 then ↑x.val else ↑x.val - ↑(namedPattern k (n + 1) h✝)) = x
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem append_append_left_iff : ∀ L, Red (L ++ L₁) (L ++ L₂) ↔ Red L₁ L₂
  | [] => Iff.rfl
  | p :: L => by simp [append_append_left_iff L, cons_cons_iff]

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
L : List (α × Bool)
⊢ Red (p :: L ++ L₁) (p :: L ++ L₂) ↔ Red L₁ L₂

Tactic:
simp [append_append_left_iff L, cons_cons_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x)
    (hh : HasDerivWithinAt h₂ h₂' t y) (hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t)
    (hy : y = f x) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
rw [hy] at hh

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
exact hh.comp_hasFDerivWithinAt x hf hst

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cofork.condition (t : Cofork f g) : f ≫ t.π = g ≫ t.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
⊢ f ≫ t.π = g ≫ t.π

Tactic:
rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem or_le : ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z

Proof state:
⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem relNorm_bot : relNorm R (⊥ : Ideal S) = ⊥

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : NoZeroSMulDivisors R S
inst✝² : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
⊢ (relNorm R) ⊥ = ⊥

Tactic:
simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_flatten (f : α → β → β) (b : β) (L : Vector (Vector α m) n) :
    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b

Proof state:
case of
α : Type u_1
β : Type u_2
m n : Nat
f : α → β → β
b : β
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ foldr f b
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    foldr (fun l b => foldr f b l) b
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }

Tactic:
simp [Array.foldr_flatten', Array.foldr_map']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m n : Nat
f : α → β → β
b : β
L : Vector (Vector α m) n
⊢ foldr f b L.flatten = foldr (fun l b => foldr f b l) b L

Tactic:
cases L using vector₂_induction

Result:
case of
α : Type u_1
β : Type u_2
m n : Nat
f : α → β → β
b : β
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ foldr f b
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    foldr (fun l b => foldr f b l) b
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiff_prod_iff (f : M → M' × N') :
    ContMDiff I (I'.prod J') n f ↔
      ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f) :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prod_mk h.2⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_11
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_12
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : WithTop ℕ∞
f : M → M' × N'
h : ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f)
⊢ ContMDiff I (I'.prod J') n f

Tactic:
convert h.1.prod_mk h.2

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_lt_encard_iff_encard_diff_lt_encard_diff (h : (s ∩ t).Finite) :
    s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard

Proof state:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard

Tactic:
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_lt_add_iff_right h.encard_lt_top.ne]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem symm_apply_mem_iff_mem_image {α β : Type*} (e : α ≃ β) (s : Set α) (x : β) :
    e.symm x ∈ s ↔ x ∈ e '' s :=
  ⟨fun h => ⟨e.symm x, h, by simp⟩, by
    rintro ⟨a, m, rfl⟩
    simpa using m⟩

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
⊢ x ∈ ⇑e '' s → e.symm x ∈ s

Tactic:
rintro ⟨a, m, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ e.symm (e a) ∈ s

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
h : e.symm x ∈ s
⊢ e (e.symm x) = x

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ e.symm (e a) ∈ s

Tactic:
simpa using m

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma cast_subConst (A B : Finset G') : (δ[A, B] : 𝕜) = #(A - B) / #A

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑δ[A, B] = ↑(#(A - B)) / ↑(#A)

Tactic:
simp [subConst]

Result:
no goals