harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem implicitFunction_hasStrictFDerivAt (g'inv : G →L[𝕜] E)
    (hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G)
    (hg'invf : φ.leftDeriv.comp g'inv = 0) :
    HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)

Proof state:
case h.e'_12
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv.comp g'inv = 0
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)
⊢ g'inv =
    (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm).comp
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))

Tactic:
simp only [ContinuousLinearMap.ext_iff, (ContinuousLinearMap.comp_apply)] at hg'inv hg'invf ⊢

Result:
case h.e'_12
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)
hg'inv : ∀ (x : G), φ.rightDeriv (g'inv x) = (ContinuousLinearMap.id 𝕜 G) x
hg'invf : ∀ (x : G), φ.leftDeriv (g'inv x) = 0 x
⊢ ∀ (x : G),
    g'inv x =
      ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm
        ((ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x)
-- Mathlib/Data/Multiset/Bind.lean
theorem prod_join [CommMonoid α] {S : Multiset (Multiset α)} :
    prod (join S) = prod (map prod S)

Proof state:
case cons
α : Type u_1
inst✝ : CommMonoid α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : s✝.join.prod = (map prod s✝).prod
⊢ (a✝ ::ₘ s✝).join.prod = (map prod (a✝ ::ₘ s✝)).prod

Tactic:
simp [ih]

Result:
no goals

Proof state:
case empty
α : Type u_1
inst✝ : CommMonoid α
⊢ (join 0).prod = (map prod 0).prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
S : Multiset (Multiset α)
⊢ S.join.prod = (map prod S).prod

Tactic:
induction S using Multiset.induction with
| empty => simp
| cons _ _ ih => simp [ih]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_pure : map₂ m (pure a) (pure b) = pure (m a b)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
⊢ map₂ m (pure a) (pure b) = pure (m a b)

Tactic:
rw [map₂_pure_right, map_pure]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem eq_of_infinite_eval_eq (p q : R[X]) (h : Set.Infinite { x | eval x p = eval x q }) :
    p = q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p = q

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p - q = 0

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ {x | (p - q).IsRoot x}.Infinite

Tactic:
simpa only [IsRoot, eval_sub, sub_eq_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p - q = 0

Tactic:
apply eq_zero_of_infinite_isRoot

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ {x | (p - q).IsRoot x}.Infinite
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem volume_image_eq_volume_div_covolume' {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L] {ι : Type*} [Fintype ι]
    (b : Basis ι ℤ L) {s : Set E} (hs : NullMeasurableSet s) :
    volume ((b.ofZLatticeBasis ℝ).equivFun '' s) = volume s / ENNReal.ofReal (covolume L)

Proof state:
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : (ι → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv ι ℝ).symm.trans ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
hf : MeasurePreserving (⇑f) volume volume
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
    volume (⇑((Basis.ofZLatticeBasis ℝ L b).map f.symm.toLinearEquiv).equivFun ∘ ⇑f.symm '' s)

Tactic:
simp only [Basis.equivFun_apply, ContinuousLinearEquiv.symm_toLinearEquiv, Basis.map_equivFun,
  LinearEquiv.symm_symm, Function.comp_apply, LinearEquiv.trans_apply,
  ContinuousLinearEquiv.coe_toLinearEquiv, ContinuousLinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/List/Lex.lean
theorem head!_le_of_lt [Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) :
    l'.head! ≤ l.head!

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) l' l
⊢ l'.head! ≤ l.head!

Tactic:
by_cases hl : l = []

Result:
case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Proof state:
case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

Tactic:
simp [hl] at h

Result:
no goals

Proof state:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
exact head_le_of_lt h

Result:
no goals

Proof state:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h

Result:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 => x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.mul_apply_eq_iff {σ τ : Perm α} (hστ : Disjoint σ τ) {a : α} :
    (σ * τ) a = a ↔ σ a = a ∧ τ a = a

Proof state:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : σ a = a ∧ τ a = a
⊢ (σ * τ) a = a

Tactic:
rw [mul_apply, h.2, h.1]

Result:
no goals

Proof state:
case inl
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hσ : σ a = a
⊢ σ a = a ∧ τ a = a

Tactic:
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩

Result:
no goals

Proof state:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
⊢ σ a = a ∧ τ a = a

Tactic:
rcases hστ a with hσ | hτ

Result:
case inl
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hσ : σ a = a
⊢ σ a = a ∧ τ a = a

case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a

Proof state:
case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a

Tactic:
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩

Result:
no goals

Proof state:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
⊢ (σ * τ) a = a ↔ σ a = a ∧ τ a = a

Tactic:
refine ⟨fun h => ?_, fun h => by rw [mul_apply, h.2, h.1]⟩

Result:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
⊢ σ a = a ∧ τ a = a
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_one {n : ℕ} : coeff (1 : R[X]) n = if n = 0 then 1 else 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if n = 0 then 1 else 0

Tactic:
simp_rw [eq_comm (a := n) (b := 0)]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if 0 = n then 1 else 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if 0 = n then 1 else 0

Tactic:
exact coeff_monomial

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem apply_dite₂ {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P]
    (a : P → α) (b : ¬P → α) (c : P → β) (d : ¬P → β) :
    f (dite P a b) (dite P c d) = dite P (fun h ↦ f (a h) (c h)) fun h ↦ f (b h) (d h)

Proof state:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma map_cyclesMap' : F.map (ShortComplex.cyclesMap' φ hl₁ hl₂) =
    ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq,  ShortComplex.LeftHomologyMapData.map_φK]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega)

Proof state:
α : Type ?u.328456
as : Array α
i : Nat
hi : i < as.reverse.size
⊢ as.size - 1 - i < as.size

Tactic:
simp at hi

Result:
α : Type ?u.328456
as : Array α
i : Nat
hi : i < as.size
⊢ as.size - 1 - i < as.size

Proof state:
case mk
α : Type u_1
i : Nat
toList✝ : List α
hi : i < { toList := toList✝ }.reverse.size
⊢ { toList := toList✝ }.reverse[i] = { toList := toList✝ }[{ toList := toList✝ }.size - 1 - i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.328456
as : Array α
i : Nat
hi : i < as.size
⊢ as.size - 1 - i < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
hi : i < as.reverse.size
⊢ as.reverse[i] = as[as.size - 1 - i]

Tactic:
cases as

Result:
case mk
α : Type u_1
i : Nat
toList✝ : List α
hi : i < { toList := toList✝ }.reverse.size
⊢ { toList := toList✝ }.reverse[i] = { toList := toList✝ }[{ toList := toList✝ }.size - 1 - i]
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem X_pow_dvd_iff {n : ℕ} {φ : R⟦X⟧} :
    (X : R⟦X⟧) ^ n ∣ φ ↔ ∀ m, m < n → coeff R m φ = 0

Proof state:
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff R m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff R m) φ = 0

Tactic:
rw [Finsupp.unique_single m]

Result:
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff R m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff R (single default (m default))) φ = 0

Proof state:
case h.e'_2.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff R m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0

Tactic:
constructor <;> intro h m hm

Result:
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff R m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff R m) φ = 0

case h.e'_2.a.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ (coeff R m) φ = 0

Proof state:
case h.e'_2.a.mpr.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ (single () m) () < n

Tactic:
simpa only [Finsupp.single_eq_same] using hm

Result:
no goals

Proof state:
case h.e'_2.a.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ (coeff R m) φ = 0

Tactic:
apply h

Result:
case h.e'_2.a.mpr.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ (single () m) () < n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ X ^ n ∣ φ ↔ ∀ m < n, (coeff R m) φ = 0

Tactic:
convert@MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ

Result:
case h.e'_2.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff R m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff R m) φ = 0

Proof state:
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff R m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff R (single default (m default))) φ = 0

Tactic:
convert h _ hm

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem surjective_rangeRestrict : Function.Surjective f.rangeRestrict

Proof state:
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy⟩

Tactic:
rw [mem_range] at hy

Result:
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩

Proof state:
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : f x ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨f x, hy⟩

Tactic:
use x

Result:
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : f x ∈ f.range
⊢ f.rangeRestrict x = ⟨f x, hy⟩

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ Function.Surjective ⇑f.rangeRestrict

Tactic:
rintro ⟨y, hy⟩

Result:
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy⟩

Proof state:
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩

Tactic:
obtain ⟨x, rfl⟩ := hy

Result:
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : f x ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨f x, hy⟩

Proof state:
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : f x ∈ f.range
⊢ f.rangeRestrict x = ⟨f x, hy⟩

Tactic:
simp only [Subtype.mk_eq_mk, rangeRestrict_apply]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.gcd_mul_right_cancel (m : Nat) (H : Coprime k n) : gcd (m * k) n = gcd m n

Proof state:
k n m : Nat
H : k.Coprime n
⊢ (m * k).gcd n = m.gcd n

Tactic:
rw [Nat.mul_comm m k, H.gcd_mul_left_cancel m]

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem cast_toZModPow (m n : ℕ) (h : m ≤ n) (x : ℤ_[p]) :
    ZMod.cast (toZModPow n x) = toZModPow m x

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = (toZModPow m) x

Tactic:
rw [← zmod_cast_comp_toZModPow _ _ h]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/Monoidal.lean
@[reassoc]
lemma leftUnitor'_inv_comm (i j : I) :
    (leftUnitor' K).inv i ≫ (tensorObj (tensorUnit C c) K).d i j =
      K.d i j ≫ (leftUnitor' K).inv j

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j

case neg
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : ¬c.Rel i j
⊢ K.leftUnitor'.inv i ≫ ((tensorUnit C c).tensorObj K).d i j = K.d i j ≫ K.leftUnitor'.inv j
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@[to_additive]
lemma orbitRel_of_subMul (p : SubMulAction R M) :
    MulAction.orbitRel R p = (MulAction.orbitRel R M).comap Subtype.val

Proof state:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
⊢ MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)

Tactic:
refine Setoid.ext_iff.2 (fun x y ↦ ?_)

Result:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (Setoid.comap Subtype.val (MulAction.orbitRel R M)) x y

Proof state:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (Setoid.comap Subtype.val (MulAction.orbitRel R M)) x y

Tactic:
rw [Setoid.comap_rel]

Result:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (MulAction.orbitRel R M) ↑x ↑y

Proof state:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
x y : ↥p
⊢ (MulAction.orbitRel R ↥p) x y ↔ (MulAction.orbitRel R M) ↑x ↑y

Tactic:
exact mem_orbit_subMul_iff

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem jd_transform [Fintype l] : (PD l R)ᵀ * JD l R * PD l R = (2 : R) • S l R

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Tactic:
have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
  simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]

Result:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Tactic:
rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]

Result:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 * 1 + 1 * 1) (1 * -1 + 1 * 1) (1 * 1 + -1 * 1) (1 * -1 + -1 * 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 * 1 + 1 * 1) (1 * -1 + 1 * 1) (1 * 1 + -1 * 1) (1 * -1 + -1 * 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)

Tactic:
simp [two_smul]

Result:
no goals

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)

Tactic:
simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {fallback : β}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
fallback : β
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback

Tactic:
simp only [getValueD_eq_getValue?]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
fallback : β
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (getValue? k (insertListConst l toInsert)).getD fallback = (getValue? k l).getD fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
fallback : β
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (getValue? k (insertListConst l toInsert)).getD fallback = (getValue? k l).getD fallback

Tactic:
rw [getValue?_insertListConst_of_contains_eq_false not_contains]

Result:
no goals