harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Equiv/Defs.lean
theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) :
    e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₂ : R₃ →+* R₂
σ₃₁ : R₃ →+* R₁
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
h : (↑e₁₂).comp f = (↑e₁₂).comp g
⊢ f = g

Tactic:
rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]

Result:
no goals

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₂ : R₃ →+* R₂
σ₃₁ : R₃ →+* R₁
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
⊢ (↑e₁₂).comp f = (↑e₁₂).comp g ↔ f = g

Tactic:
refine ⟨fun h => ?_, congrArg e₁₂.comp⟩

Result:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₂ : R₃ →+* R₂
σ₃₁ : R₃ →+* R₁
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
h : (↑e₁₂).comp f = (↑e₁₂).comp g
⊢ f = g
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaULiftEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : Sheaf J (Type (max v v')))
    (x : F.val.obj ⟨X⟩) : J.yonedaULift.map f ≫ J.yonedaULiftEquiv.symm x = J.yonedaULiftEquiv.symm
      ((F.val.map f.op) x)

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f ≫ J.yonedaULiftEquiv.symm x) =
    J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm (F.val.map f.op x))

Tactic:
simp only [yonedaULiftEquiv_comp, Equiv.apply_symm_apply]

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ (J.yonedaULiftEquiv.symm x).val.app (op X') (J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f)) = F.val.map f.op x

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ (yonedaULift.{v', v, u} J).map f ≫ J.yonedaULiftEquiv.symm x = J.yonedaULiftEquiv.symm (F.val.map f.op x)

Tactic:
apply J.yonedaULiftEquiv.injective

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f ≫ J.yonedaULiftEquiv.symm x) =
    J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm (F.val.map f.op x))

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ (J.yonedaULiftEquiv.symm x).val.app (op X') { down := f } = F.val.map f.op x

Tactic:
rfl

Result:
no goals

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ (J.yonedaULiftEquiv.symm x).val.app (op X') (J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f)) = F.val.map f.op x

Tactic:
rw [yonedaULiftEquiv_yonedaULift_map]

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.val.obj (op X)
⊢ (J.yonedaULiftEquiv.symm x).val.app (op X') { down := f } = F.val.map f.op x
-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem concat_left (hb : f ⊤ = g ⊥) {t : Icc a c} (ht : t ≤ b) :
    concat f g t = f ⟨t, t.2.1, ht⟩

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : ↑t ≤ b
⊢ (f.concat g) t = f ⟨↑t, ⋯⟩

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionLeft hb]

Result:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : ↑t ≤ b
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionLeft) ⟨↑t, ⋯⟩

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : ↑t ≤ b
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionLeft) ⟨↑t, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn_yield_eq_foldl
    (l : Vector α n) (f : α → β → β) (init : β) :
    forIn (m := Id) l init (fun a b => .yield (f a b)) =
      l.foldl (fun b a => f a b) init

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β → β
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a b => ForInStep.yield (f a b)) =
    foldl (fun b a => f a b) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β → β
init : β
⊢ (forIn l init fun a b => ForInStep.yield (f a b)) = foldl (fun b a => f a b) init l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β → β
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a b => ForInStep.yield (f a b)) =
    foldl (fun b a => f a b) init { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Data/Part.lean
theorem bind_some_right (x : Part α) : x.bind some = x

Proof state:
α : Type u_1
x : Part α
⊢ map (fun y => y) x = x

Tactic:
simp [map_id']

Result:
no goals

Proof state:
α : Type u_1
x : Part α
⊢ x.bind some = x

Tactic:
erw [bind_some_eq_map]

Result:
α : Type u_1
x : Part α
⊢ map (fun y => y) x = x
-- Mathlib/CategoryTheory/Limits/Types.lean
@[simp]
lemma quotToQuotUlift_ι (F : J ⥤ Type u) (j : J) (x : F.obj j) :
    quotToQuotUlift F (Quot.ι F j x) = Quot.ι _ j (ULift.up x)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
j : J
x : F.obj j
⊢ quotToQuotUlift F (Quot.ι F j x) = Quot.ι (F ⋙ uliftFunctor.{u_1, u}) j { down := x }

Tactic:
dsimp [quotToQuotUlift, Quot.ι]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma mul_dvd_mul : a ∣ b → c ∣ d → a * c ∣ b * d
  | ⟨e, he⟩, ⟨f, hf⟩ => ⟨e * f, by simp [he, hf, Int.mul_assoc, Int.mul_left_comm, Nat.mul_comm]⟩

Proof state:
a b c d e : ℤ
he : b = a * e
f : ℤ
hf : d = c * f
⊢ b * d = a * c * (e * f)

Tactic:
simp [he, hf, Int.mul_assoc, Int.mul_left_comm, Nat.mul_comm]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem coe_iInf {ι : Sort*} (S : ι → IntermediateField F E) : (↑(iInf S) : Set E) = ⋂ i, S i

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_3
S : ι → IntermediateField F E
⊢ ↑(iInf S) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem bddBelow_upperClosure : BddBelow (upperClosure s : Set α) ↔ BddBelow s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow ↑(upperClosure s) ↔ BddBelow s

Tactic:
simp_rw [BddBelow, lowerBounds_upperClosure]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_map_equiv {f : R ≃+* S} {K : Subsemiring R} {x : S} :
    x ∈ K.map (f : R →+* S) ↔ f.symm x ∈ K

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R ≃+* S
K : Subsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ f.symm x ∈ K

Tactic:
convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x using 1

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_algebraMap [StrongRankCondition R] [Module.Free R S] (x : R) :
    trace R S (algebraMap R S x) = finrank R S • x

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

Tactic:
rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

Tactic:
simp [trace_eq_zero_of_not_exists_basis R H, finrank_eq_zero_of_not_exists_basis_finset H]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

Tactic:
by_cases H : ∃ s : Finset S, Nonempty (Basis s R S)

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x
-- Mathlib/Analysis/Analytic/Basic.lean
theorem FormalMultilinearSeries.hasFPowerSeriesOnBall [CompleteSpace F]
    (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
    HasFPowerSeriesOnBall p.sum p 0 p.radius :=
  { r_le := le_rfl
    r_pos := h
    hasSum := fun hy => by
      rw [zero_add]
      exact p.hasSum hy }

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ EMetric.ball 0 p.radius
⊢ HasSum (fun n => (p n) fun x => y✝) (p.sum (0 + y✝))

Tactic:
rw [zero_add]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ EMetric.ball 0 p.radius
⊢ HasSum (fun n => (p n) fun x => y✝) (p.sum y✝)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ EMetric.ball 0 p.radius
⊢ HasSum (fun n => (p n) fun x => y✝) (p.sum y✝)

Tactic:
exact p.hasSum hy

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_mono_left (ha : a ≤ a') (hr : r ≤ 1) : lineMap a b r ≤ lineMap a' b r

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b

Tactic:
exact add_le_add_right (smul_le_smul_of_nonneg_left ha (sub_nonneg.2 hr)) _

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (lineMap a b) r ≤ (lineMap a' b) r

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b : E
r : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc]
lemma g_s (s : S.Splitting) : S.g ≫ s.s = 𝟙 _ - s.r ≫ S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f

Tactic:
rw [← s.id, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma odd_iff : Odd n ↔ n % 2 = 1 where
  mp := fun ⟨m, hm⟩ ↦ by simp [hm, add_emod]
  mpr h := ⟨n / 2, by rw [← h, add_comm, emod_add_ediv n 2]⟩

Proof state:
n : ℤ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
rw [← h, add_comm, emod_add_ediv n 2]

Result:
no goals

Proof state:
n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
simp [hm, add_emod]

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem free_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M]
    (H : Function.Injective ((𝔪).subtype.rTensor M)) :
    Module.Free R M

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
w✝¹ : Type u_2
w✝ : w✝¹ → M
b : Basis w✝¹ R M
h✝ : ∀ (i : w✝¹), b i = id (w✝ i)
⊢ Free R M

Tactic:
exact Free.of_basis b

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ Free R M

Tactic:
obtain ⟨_, _, b, _⟩ := exists_basis_of_span_of_maximalIdeal_rTensor_injective H id (by simp)

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
w✝¹ : Type u_2
w✝ : w✝¹ → M
b : Basis w✝¹ R M
h✝ : ∀ (i : w✝¹), b i = id (w✝ i)
⊢ Free R M

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ Submodule.span R (Set.range id) = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toReal = ⨆ i, (f i).toReal

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ (iSup f).toReal = ⨆ i, (f i).toReal

Tactic:
simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem mul_adjp_apply_eq : (A * adjp s A) i i = detp s A

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key :
  ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) =
    ∑ i ∈ filter (fun i_1 => i_1 i ∈ univ) (ofSign s), ∏ k : n, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Tactic:
simp_rw [mem_univ, filter_True] at key

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Tactic:
simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
⊢ ∑ x : n, ∑ i_1 ∈ filter (fun x_1 => x_1 i = x) (ofSign s), A i x * ∏ k ∈ {i}ᶜ, A k (i_1 k) =
    ∑ j : n, ∑ σ ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (σ k)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
⊢ ∑ x : n, ∑ i_1 ∈ filter (fun x_1 => x_1 i = x) (ofSign s), A i x * ∏ k ∈ {i}ᶜ, A k (i_1 k) =
    ∑ j : n, ∑ σ ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (σ k)

Tactic:
refine sum_congr rfl fun x hx ↦ sum_congr rfl fun σ hσ ↦ ?_

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ filter (fun i_1 => i_1 i = x) (ofSign s)
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = ∏ k : n, A k (σ k)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j : n, ∑ i ∈ filter (fun i_1 => i_1 i = j) (ofSign s), ∏ k : n, A k (i k) = ∑ i ∈ ofSign s, ∏ k : n, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ filter (fun i_1 => i_1 i = x) (ofSign s)
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = ∏ k : n, A k (σ k)

Tactic:
rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem le_tsub_add_add : a + b ≤ a - c + (b + c)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a ≤ b + c + (a - c)

Tactic:
exact add_le_add_add_tsub

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)

Tactic:
rw [add_comm a, add_comm (a - c)]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a ≤ b + c + (a - c)
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
lemma not_mem_neighborSet_self : a ∉ G.neighborSet a

Proof state:
V : Type u
G : SimpleGraph V
a : V
⊢ a ∉ G.neighborSet a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} :
    get! (m.erase k) a = if k == a then default else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k a : α
⊢ get! (m.erase k) a = if (k == a) = true then default else get! m a

Tactic:
simp_to_raw using Raw₀.Const.get!_erase

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Finite.einfsep (hs : s.Finite) : s.einfsep = hs.offDiag.toFinset.inf (uncurry edist)

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
⊢ s.einfsep = ⋯.toFinset.inf (uncurry edist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)

Tactic:
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_then_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
    (@ite _ p h (!decide p) q) = (!decide p && q)

Proof state:
p : Prop
h w : Decidable p
q : Bool
⊢ (if p then !decide p else q) = (!decide p && q)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem exists_mem_insert (a : α) (s : Finset α) (p : α → Prop) :
    (∃ x, x ∈ insert a s ∧ p x) ↔ p a ∨ ∃ x, x ∈ s ∧ p x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

Tactic:
simp only [mem_insert, or_and_right, exists_or, exists_eq_left]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem annihilator_isRadical (R) [CommRing R] [Module R M] [IsSemisimpleModule R M] :
    (Module.annihilator R M).IsRadical

Proof state:
M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (Module.annihilator R M).IsRadical

Tactic:
rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]

Result:
M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (⨅ i, (↑i).annihilator).IsRadical

Proof state:
M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (⨅ i, (↑i).annihilator).IsRadical

Tactic:
exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.disjoint_nhdsSet_right {l : Filter X} (hs : IsCompact s) :
    Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Tactic:
simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma pushoutCocone_inl_eq_inr_imp_of_iso {c c' : PushoutCocone f g} (e : c ≅ c')
    (x₁ : X₁) (x₂ : X₂) (h : c.inl x₁ = c.inr x₂) :
    c'.inl x₁ = c'.inr x₂

Proof state:
case h.e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : c.inl x₁ = c.inr x₂
⊢ c'.inr x₂ = e.hom.hom (c.inr x₂)

Tactic:
exact congr_fun (e.hom.w WalkingSpan.right).symm x₂

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : c.inl x₁ = c.inr x₂
⊢ c'.inl x₁ = c'.inr x₂

Tactic:
convert congr_arg e.hom.hom h

Result:
case h.e'_2
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : c.inl x₁ = c.inr x₂
⊢ c'.inl x₁ = e.hom.hom (c.inl x₁)

case h.e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : c.inl x₁ = c.inr x₂
⊢ c'.inr x₂ = e.hom.hom (c.inr x₂)

Proof state:
case h.e'_2
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : c.inl x₁ = c.inr x₂
⊢ c'.inl x₁ = e.hom.hom (c.inl x₁)

Tactic:
exact congr_fun (e.hom.w WalkingSpan.left).symm x₁

Result:
no goals