harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_tail? {s : Heap α} (h : s.NoSibling) : s.tail? le = some s' →
    s.size = s'.size + 1

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
⊢ tail? le s = some s' → s.size = s'.size + 1

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s.size = s'.size + 1

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s.size = s'.size + 1

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact size_deleteMin h eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
a : α
tl : Heap α
eq₂ : deleteMin le s = some (a, tl)
⊢ s.size = ((fun x => x.snd) (a, tl)).size + 1

Tactic:
exact size_deleteMin h eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s.size = s'.size + 1

Tactic:
intro eq

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
h : s.NoSibling
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s.size = s'.size + 1
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusMap_sub_center (c : ℂⁿ) (R : ℝⁿ) (θ : ℝⁿ) : torusMap c R θ - c = torusMap 0 R θ

Proof state:
case h
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
i : Fin n
⊢ (torusMap c R θ - c) i = torusMap 0 R θ i

Tactic:
simp [torusMap]

Result:
no goals

Proof state:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ - c = torusMap 0 R θ

Tactic:
ext1 i

Result:
case h
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
i : Fin n
⊢ (torusMap c R θ - c) i = torusMap 0 R θ i
-- Mathlib/Data/Multiset/Bind.lean
theorem cons_bind : (a ::ₘ s).bind f = f a + s.bind f

Proof state:
α : Type u_1
β : Type v
a : α
s : Multiset α
f : α → Multiset β
⊢ (a ::ₘ s).bind f = f a + s.bind f

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateFrom_eq {s : Set (Set α)} (hs : IsPiSystem s) :
    generateFrom s = (generate s).toMeasurableSpace fun _ _ => generate_inter hs :=
  le_antisymm (generateFrom_le fun t ht => GenerateHas.basic t ht)
    (ofMeasurableSpace_le_ofMeasurableSpace_iff.mp <| by
      rw [ofMeasurableSpace_toMeasurableSpace]
      exact generate_le _ fun t ht => measurableSet_generateFrom ht)

Proof state:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)

Tactic:
exact generate_le _ fun t ht => measurableSet_generateFrom ht

Result:
no goals

Proof state:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)

Tactic:
rw [ofMeasurableSpace_toMeasurableSpace]

Result:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
/-- If a linear map preserves the quadratic forms and is surjective, then the algebra
maps it induces between Clifford algebras is also surjective. -/
lemma map_surjective {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂)
    (hf : Function.Surjective f) : Function.Surjective (CliffordAlgebra.map f) :=
  CliffordAlgebra.induction
    (fun r ↦ ⟨algebraMap R (CliffordAlgebra Q₁) r, by simp only [AlgHom.commutes]⟩)
    (fun y ↦ let ⟨x, hx⟩ := hf y; ⟨CliffordAlgebra.ι Q₁ x, by simp only [map_apply_ι, hx]⟩)
    (fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x * y, by simp only [map_mul, hx, hy]⟩)
    (fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x + y, by simp only [map_add, hx, hy]⟩)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
y : M₂
x : M₁
hx : f x = y
⊢ (map f) ((ι Q₁) x) = (ι Q₂) y

Tactic:
simp only [map_apply_ι, hx]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
x✝³ x✝² : CliffordAlgebra Q₂
x✝¹ : ∃ a, (map f) a = x✝³
x✝ : ∃ a, (map f) a = x✝²
x : CliffordAlgebra Q₁
hx : (map f) x = x✝³
y : CliffordAlgebra Q₁
hy : (map f) y = x✝²
⊢ (map f) (x * y) = x✝³ * x✝²

Tactic:
simp only [map_mul, hx, hy]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
r : R
⊢ (map f) ((algebraMap R (CliffordAlgebra Q₁)) r) = (algebraMap R (CliffordAlgebra Q₂)) r

Tactic:
simp only [AlgHom.commutes]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
x✝³ x✝² : CliffordAlgebra Q₂
x✝¹ : ∃ a, (map f) a = x✝³
x✝ : ∃ a, (map f) a = x✝²
x : CliffordAlgebra Q₁
hx : (map f) x = x✝³
y : CliffordAlgebra Q₁
hy : (map f) y = x✝²
⊢ (map f) (x + y) = x✝³ + x✝²

Tactic:
simp only [map_add, hx, hy]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶ Y) :
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom =
      (normalizeIsoApp' C X n).hom ≫
        inclusion.map (eqToHom (Discrete.ext (normalizeObj_congr n f)))

Proof state:
case id
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X✝ ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).hom ≫ (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).inv ≫ (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).inv ≫ (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
all_goals simp

Result:
no goals

Proof state:
C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ h ▷ η' ≫ (normalizeIsoApp' C (Y ⊗ η') n).hom =
    (normalizeIsoApp' C (X ⊗ η') n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
  Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]

Result:
C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ h ▷ η' ≫
      (α_ (inclusionObj n) Y η').inv ≫
        (normalizeIsoApp' C Y n).hom ▷ η' ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X η').inv ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ (normalizeIsoApp' C η' (X.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
-- Mathlib/Data/List/Basic.lean
theorem getLast?_append_cons :
    ∀ (l₁ : List α) (a : α) (l₂ : List α), getLast? (l₁ ++ a :: l₂) = getLast? (a :: l₂)
  | [], _, _ => rfl
  | [_], _, _ => rfl
  | b :: c :: l₁, a, l₂ => by rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]

Proof state:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
rw [cons_append, cons_append, getLast?_cons_cons,
← cons_append, getLast?_append_cons (c :: l₁)]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictVar [DecidableEq α] {t : L.Term α} {f : t.varFinset → β}
    {v : β → M} (v' : α → M) (hv' : ∀ a, v (f a) = v' a) :
    (t.restrictVar f).realize v = t.realize v'

Proof state:
case func
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : { x // x ∈ (_ts✝ a).varFinset } → β},
    (∀ (a_1 : { x // x ∈ (_ts✝ a).varFinset }), v (f a_1) = v' ↑a_1) →
      realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : { x // x ∈ (func _f✝ _ts✝).varFinset } → β
hv' : ∀ (a : { x // x ∈ (func _f✝ _ts✝).varFinset }), v (f a) = v' ↑a
⊢ realize v ((func _f✝ _ts✝).restrictVar f) = realize v' (func _f✝ _ts✝)

Tactic:
exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Result:
no goals

Proof state:
case var
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
a✝ : α
f : { x // x ∈ (var a✝).varFinset } → β
hv' : ∀ (a : { x // x ∈ (var a✝).varFinset }), v (f a) = v' ↑a
⊢ realize v ((var a✝).restrictVar f) = realize v' (var a✝)

Tactic:
simp [restrictVar, hv']

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : { x // x ∈ (_ts✝ a).varFinset } → β},
    (∀ (a_1 : { x // x ∈ (_ts✝ a).varFinset }), v (f a_1) = v' ↑a_1) →
      realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : { x // x ∈ (func _f✝ _ts✝).varFinset } → β
hv' : ∀ (a : { x // x ∈ (func _f✝ _ts✝).varFinset }), v (f a) = v' ↑a
i : Fin l✝
⊢ ∀ (a : { x // x ∈ (_ts✝ i).varFinset }), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

Tactic:
simp [Function.comp_apply, hv']

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : L.Term α
f : { x // x ∈ t.varFinset } → β
v : β → M
v' : α → M
hv' : ∀ (a : { x // x ∈ t.varFinset }), v (f a) = v' ↑a
⊢ realize v (t.restrictVar f) = realize v' t

Tactic:
induction t with
| var => simp [restrictVar, hv']
| func _ _ ih =>
  exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_isField (H : IsField (A ⊗[R] B)) : A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
⊢ Function.Injective ⇑(A.mulMap B)

Tactic:
letI : Field (A ⊗[R] B) := H.toField

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this : Field (↥A ⊗[R] ↥B) := H.toField
⊢ Function.Injective ⇑(A.mulMap B)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
⊢ A.LinearDisjoint B

Tactic:
nontriviality S

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
⊢ A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this : Field (↥A ⊗[R] ↥B) := H.toField
⊢ Function.Injective ⇑(A.mulMap B)

Tactic:
letI : NonAssocRing (A ⊗[R] B) := Ring.toNonAssocRing

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this✝ : Field (↥A ⊗[R] ↥B) := H.toField
this : NonAssocRing (↥A ⊗[R] ↥B) := Ring.toNonAssocRing
⊢ Function.Injective ⇑(A.mulMap B)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
⊢ A.LinearDisjoint B

Tactic:
rw [linearDisjoint_iff_injective]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
⊢ Function.Injective ⇑(A.mulMap B)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this✝ : Field (↥A ⊗[R] ↥B) := H.toField
this : NonAssocRing (↥A ⊗[R] ↥B) := Ring.toNonAssocRing
⊢ Function.Injective ⇑(A.mulMap B)

Tactic:
exact RingHom.injective _

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem repeat_succ (a : Fin n → α) (m : ℕ) :
    Fin.repeat m.succ a =
      append a (Fin.repeat m a) ∘ Fin.cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..))

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Proof state:
case h.refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
l : Fin n
⊢ «repeat» m.succ a (Fin.cast ⋯ (castAdd (m * n) l)) =
    (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m * n) l))

Tactic:
simp [modNat, Nat.mod_eq_of_lt l.is_lt]

Result:
no goals

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h

Tactic:
apply funext

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (m.succ * n)), «repeat» m.succ a x = (append a («repeat» m a) ∘ Fin.cast h) x

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯

Tactic:
generalize_proofs h

Result:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast h

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
refine Fin.addCases (fun l => ?_) fun r => ?_

Result:
case h.refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
l : Fin n
⊢ «repeat» m.succ a (Fin.cast ⋯ (castAdd (m * n) l)) =
    (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m * n) l))

case h.refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Proof state:
case h.refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Tactic:
simp [modNat]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Basic.lean
theorem of_isoOfHomeo {X Y : TopCat.{u}} (f : X ≃ₜ Y) : homeoOfIso (isoOfHomeo f) = f

Proof state:
case H
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : ↑X
⊢ (homeoOfIso (isoOfHomeo f)) x✝ = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ homeoOfIso (isoOfHomeo f) = f

Tactic:
ext

Result:
case H
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : ↑X
⊢ (homeoOfIso (isoOfHomeo f)) x✝ = f x✝
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_mul [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
rw [← this, add_sub_cancel_right]

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
rw [sub_add_cancel] at this

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
-- Mathlib/Data/ENNReal/Order.lean
theorem natCast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞)

Proof state:
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_adjoin_coe_preimage {s : Set A} : adjoin R (((↑) : adjoin R s → A) ⁻¹' s) = ⊤

Proof state:
case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact Subalgebra.algebraMap_mem _ r

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ adjoin R (Subtype.val ⁻¹' s) = ⊤

Tactic:
refine eq_top_iff.2 fun ⟨x, hx⟩ ↦
    adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) hx

Result:
case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Proof state:
case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact Subalgebra.mul_mem _

Result:
no goals

Proof state:
case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact Subalgebra.add_mem _

Result:
no goals

Proof state:
case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact subset_adjoin ha

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem mul_right (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n]

Proof state:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
rw [mul_comm a, mul_comm b]

Result:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Proof state:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Tactic:
exact h.mul_left c

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem Tendsto.of_tendsto_comp {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ}
    (hfg : Tendsto (g ∘ f) a c) (hg : comap g c ≤ b) : Tendsto f a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b

Tactic:
calc
  a ≤ comap (g ∘ f) c := hfg
  _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b

Tactic:
rw [tendsto_iff_comap] at hfg ⊢

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ comap (g ∘ f) c ≤ comap f b

Tactic:
simpa [comap_comap] using comap_mono hg

Result:
no goals
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n)
    (A : Finset (ℕ × ℕ)) (hAn : A ⊆ range n ×ˢ range n) (hAε : ε * n ^ 2 ≤ #A) :
    ¬ IsCornerFree (A : Set (ℕ × ℕ))

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ ↑(#A) = ↑(#(image (Prod.map Nat.cast Nat.cast) A))

Tactic:
rw [card_image_of_injOn]

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))
this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)
⊢ Set.InjOn (Prod.map Nat.cast Nat.cast) ↑A
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_of_lt_mul_right₀ [MulPosReflectLT α] (hb : 0 ≤ b) (h : b < a * b) : 1 < a :=
  lt_of_mul_lt_mul_right (by simpa) hb

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
hb : 0 ≤ b
h : b < a * b
⊢ 1 * b < a * b

Tactic:
simpa

Result:
no goals