harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_basis_left {ι : Type*} (a : Basis ι F A)
    (H : LinearIndependent L (A.val ∘ a)) : A.LinearDisjoint L :=
  Subalgebra.LinearDisjoint.of_basis_left _ _ a <| H.map_of_surjective_injective
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) (AddMonoidHom.id E)
    (AlgEquiv.surjective _) (by simp) (fun _ _ ↦ by simp_rw [Algebra.smul_def]; rfl)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
simp

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) (x✝¹ • x✝) =
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((algebraMap L E) x✝¹ * x✝) =
    (algebraMap (↥(IsScalarTower.toAlgHom F L E).range) E)
        ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹) *
      (AddMonoidHom.id E) x✝

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((algebraMap L E) x✝¹ * x✝) =
    (algebraMap (↥(IsScalarTower.toAlgHom F L E).range) E)
        ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹) *
      (AddMonoidHom.id E) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem BiconeMorphism.ext {c c' : Bicone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Proof state:
case mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom = g.hom
⊢ { hom := hom✝, wπ := wπ✝, wι := wι✝ } = g

Tactic:
cases g

Result:
case mk.mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
hom✝¹ : c.pt ⟶ c'.pt
wπ✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π j = c.π j
wι✝¹ : ∀ (j : J), c.ι j ≫ hom✝¹ = c'.ι j
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ }.hom = { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom
⊢ { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ } = { hom := hom✝, wπ := wπ✝, wι := wι✝ }

Proof state:
case mk.mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
hom✝¹ : c.pt ⟶ c'.pt
wπ✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π j = c.π j
wι✝¹ : ∀ (j : J), c.ι j ≫ hom✝¹ = c'.ι j
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ }.hom = { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom
⊢ { hom := hom✝¹, wπ := wπ✝¹, wι := wι✝¹ } = { hom := hom✝, wπ := wπ✝, wι := wι✝ }

Tactic:
congr

Result:
no goals

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Result:
case mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom = g.hom
⊢ { hom := hom✝, wπ := wπ✝, wι := wι✝ } = g
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
lemma ne_nat (z : ℍ) : ∀ n : ℕ, z.1 ≠ n

Proof state:
z : ℍ
⊢ ∀ (n : ℕ), ↑z ≠ ↑n

Tactic:
intro n

Result:
z : ℍ
n : ℕ
⊢ ↑z ≠ ↑n

Proof state:
z : ℍ
n : ℕ
h1 : 0 < (↑z).im
⊢ ↑z ≠ ↑n

Tactic:
aesop

Result:
no goals

Proof state:
z : ℍ
n : ℕ
⊢ ↑z ≠ ↑n

Tactic:
have h1 := z.2

Result:
z : ℍ
n : ℕ
h1 : 0 < (↑z).im
⊢ ↑z ≠ ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.ge_ule (x y : BitVec w) : x ≥ y ↔ ((!x.ult y) = true)

Proof state:
w : Nat
x y : BitVec w
⊢ x ≥ y ↔ (!x.ult y) = true

Tactic:
simp [BitVec.le_ult]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_length_mul (l : List α) : ∀ n : ℕ, l.rotate' (l.length * n) = l
  | 0 => by simp
  | n + 1 =>
    calc
      l.rotate' (l.length * (n + 1)) =
          (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (l.length * (n + 1)) = (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length

Tactic:
simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ l.rotate' (l.length * 0) = l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length = l

Tactic:
rw [rotate'_length, rotate'_length_mul l n]

Result:
no goals
-- Mathlib/Algebra/Lie/CartanSubalgebra.lean
lemma ne_bot_of_isCartanSubalgebra [Nontrivial L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
    H ≠ ⊥

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H ≠ ⊥

Tactic:
intro e

Result:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
⊢ False

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ False

Tactic:
have : x ∈ H.normalizer := by simp [LieSubalgebra.mem_normalizer_iff, e]

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ False

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : L)

Result:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ False

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ x ∈ H.normalizer

Tactic:
simp [LieSubalgebra.mem_normalizer_iff, e]

Result:
no goals

Proof state:
case intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ False

Tactic:
exact hx (by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this)

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ x = 0

Tactic:
rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ c pa,
      (∀ᶠ (x : β) in l', pa x) ∧
        ∃ pb,
          (∀ᶠ (y : α) in l, pb y) ∧
            ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ c pa,
      (∀ᶠ (x : β) in l', pa x) ∧
        ∃ pb,
          (∀ᶠ (y : α) in l, pb y) ∧
            ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.eval_norm (ctx : Context α) (e : Expr) : evalList α ctx (norm ctx e) = eval α ctx e

Proof state:
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx
      (if ContextInformation.isIdem ctx = true then
        mergeIdem
          (if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx e.toList)
          else removeNeutrals ctx e.toList)
      else
        if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx e.toList)
        else removeNeutrals ctx e.toList) =
    eval α ctx e

Tactic:
cases h₁ : ContextInformation.isIdem ctx <;> cases h₂ : ContextInformation.isComm ctx <;>
simp_all [evalList_removeNeutrals, eval_toList, toList_nonEmpty, evalList_mergeIdem, evalList_sort]

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx (norm ctx e) = eval α ctx e

Tactic:
simp [norm]

Result:
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx
      (if ContextInformation.isIdem ctx = true then
        mergeIdem
          (if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx e.toList)
          else removeNeutrals ctx e.toList)
      else
        if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx e.toList)
        else removeNeutrals ctx e.toList) =
    eval α ctx e
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
    (h : m.WF) (he : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
he : (k == k') = true
⊢ k' ∈ alter m k f ↔ (f (get? m k)).isSome = true

Tactic:
rw [mem_alter h, if_pos he]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[reassoc]
lemma stalkMap_congr_hom (f g : X ⟶ Y) (hfg : f = g) (x : X) :
    f.stalkMap x = Y.presheaf.stalkSpecializes (specializes_of_eq <| hfg ▸ rfl) ≫
      g.stalkMap x

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x

Tactic:
subst hfg

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_of_perm [EquivBEq α] {a : α} {f : Option β → Option β} {l l' : List ((_ : α) × β)}
    (hl : DistinctKeys l) (hp : Perm l l') :
    Perm (alterKey a f l) (alterKey a f l')

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (match f (getValue? a l') with
      | none => eraseKey a l
      | some v => insertEntry a v l).Perm
    (match f (getValue? a l') with
    | none => eraseKey a l'
    | some v => insertEntry a v l')

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option β
heq✝ : f (getValue? a l') = none
⊢ (eraseKey a l).Perm (eraseKey a l')

case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a l') = some v✝
⊢ (insertEntry a v✝ l).Perm (insertEntry a v✝ l')

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a l') = some v✝
⊢ (insertEntry a v✝ l).Perm (insertEntry a v✝ l')

Tactic:
exact insertEntry_of_perm hl hp

Result:
no goals

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
x✝ : Option β
heq✝ : f (getValue? a l') = none
⊢ (eraseKey a l).Perm (eraseKey a l')

Tactic:
exact eraseKey_of_perm hl hp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (alterKey a f l).Perm (alterKey a f l')

Tactic:
simp only [alterKey, getValue?_of_perm hl hp]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l l' : List ((_ : α) × β)
hl : DistinctKeys l
hp : l.Perm l'
⊢ (match f (getValue? a l') with
      | none => eraseKey a l
      | some v => insertEntry a v l).Perm
    (match f (getValue? a l') with
    | none => eraseKey a l'
    | some v => insertEntry a v l')
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem max_zero_add_max_neg_zero_eq_abs_self (a : α) : max a 0 + max (-a) 0 = |a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a| = a ⊔ 0 + -a ⊔ 0

Tactic:
rcases le_total 0 a with (ha | ha) <;> simp [ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ a ⊔ 0 + -a ⊔ 0 = |a|

Tactic:
symm

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a| = a ⊔ 0 + -a ⊔ 0
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma baseChange_mul (f g : Module.End R M) :
    (f * g).baseChange A = f.baseChange A * g.baseChange A

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f * g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f * baseChange A g)) 1) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
⊢ baseChange A (f * g) = baseChange A f * baseChange A g

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f * g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f * baseChange A g)) 1) x✝
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Tactic:
rw [abs_mul_abs_self]

Result:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b

Tactic:
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
  neg_add_rev, neg_neg, add_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem counit_comul_hom (M : Bimon_ C) :
    M.comul.hom ≫ (M.counit.hom ▷ _) = (λ_ _).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.comul.hom ≫ M.counit.hom ▷ M.X.X = (λ_ M.X.X).inv

Tactic:
simpa [- Comon_.counit_comul] using congr_arg Mon_.Hom.hom M.counit_comul

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem map_apply' (κ : Kernel α β) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    map κ f a s = κ a (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ.map f) a) s = (κ a) (f ⁻¹' s)

Tactic:
rw [map_apply _ hf, Measure.map_apply hf hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem mapM_congr [Monad m] {as bs : Vector α n} (w : as = bs)
    {f : α → m β} :
    as.mapM f = bs.mapM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
as : Vector α n
f : α → m β
⊢ mapM f as = mapM f as

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
as bs : Vector α n
w : as = bs
f : α → m β
⊢ mapM f as = mapM f bs

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
as : Vector α n
f : α → m β
⊢ mapM f as = mapM f as
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_apply_apply_zpow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ (f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x

Tactic:
rw [SameCycle.cycleOf_apply]

Result:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = (f ^ (k + 1)) x

α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Tactic:
exact ⟨k, rfl⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = (f ^ (k + 1)) x

Tactic:
rw [add_comm, zpow_add, zpow_one, mul_apply]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem mono_cast : Monotone (Nat.cast : ℕ → α) :=
  monotone_nat_of_le_succ fun n ↦ by
    rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1

Tactic:
exact le_add_of_nonneg_right zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)

Tactic:
rw [Nat.cast_succ]

Result:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_id (F : J ⥤ C) :
    colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = colim.map F.leftUnitor.hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem mkRingHom_surjective (r : R → R → Prop) : Function.Surjective (mkRingHom r)

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective ⇑(mkRingHom r)

Tactic:
simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel r) x }

Proof state:
case mk.mk
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ∃ a, (fun x => { toQuot := Quot.mk (Rel r) x }) a = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel r) x }

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.mk
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ∃ a, (fun x => { toQuot := Quot.mk (Rel r) x }) a = { toQuot := Quot.mk (Rel r) a✝ }
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x.toENNReal = y.toENNReal ↔ x = y

Proof state:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x.toENNReal = y.toENNReal ↔ x = y

Tactic:
induction x <;> induction y <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_empty [Monad m] (f : α → β → m β) (init : β) :
    foldrM f init #[] start stop = return init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start stop : Nat
inst✝ : Monad m
f : α → β → m β
init : β
⊢ foldrM f init #[] start stop = pure init

Tactic:
simp [foldrM]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_norm_left : IsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g

Tactic:
simp only [IsBigOWith_def, norm_norm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rootD_ext {m1 m2 : UnionFind}
    (H : ∀ x, m1.parent x = m2.parent x) {x} : m1.rootD x = m2.rootD x

Proof state:
m1 m2 : UnionFind
H : ∀ (x : Nat), m1.parent x = m2.parent x
x : Nat
h : m2.parent x = x
⊢ m1.rootD x = m2.rootD x

Tactic:
rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]

Result:
no goals

Proof state:
m1 m2 : UnionFind
H : ∀ (x : Nat), m1.parent x = m2.parent x
x : Nat
h : ¬m2.parent x = x
this : m2.rankMax - m2.rank (m2.parent x) < m2.rankMax - m2.rank x
⊢ m1.rootD x = m2.rootD x

Tactic:
rw [← rootD_parent, H, rootD_ext H, rootD_parent]

Result:
no goals

Proof state:
m1 m2 : UnionFind
H : ∀ (x : Nat), m1.parent x = m2.parent x
x : Nat
h : ¬m2.parent x = x
⊢ m1.rootD x = m2.rootD x

Tactic:
have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)

Result:
m1 m2 : UnionFind
H : ∀ (x : Nat), m1.parent x = m2.parent x
x : Nat
h : ¬m2.parent x = x
this : m2.rankMax - m2.rank (m2.parent x) < m2.rankMax - m2.rank x
⊢ m1.rootD x = m2.rootD x

Proof state:
m1 m2 : UnionFind
H : ∀ (x : Nat), m1.parent x = m2.parent x
x : Nat
⊢ m1.rootD x = m2.rootD x

Tactic:
if h : m2.parent x = x then
  rw [rootD_eq_self.2 h, rootD_eq_self.2 ((H _).trans h)]
else
  have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
  rw [← rootD_parent, H, rootD_ext H, rootD_parent]

Result:
no goals