harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem HasProd.update (hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) :
    HasProd (update f b a) (a / f b * a₁)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
rw [h, update_self]

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a / f b else 1) * f b

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
⊢ HasProd (Function.update f b a) (a / f b * a₁)

Tactic:
convert (hasProd_ite_eq b (a / f b)).mul hf with b'

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
by_cases h : b' = b

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

case neg
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a₁ : α
hf : HasProd f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a / f b else 1) * f b

Tactic:
simp [eq_self_iff_true, if_true, sub_add_cancel]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem ext_inner_left {x y : E} (h : ∀ v, ⟪v, x⟫ = ⟪v, y⟫) : x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), inner v x = inner v y
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]

Result:
no goals
-- Mathlib/Logic/Relation.lean
@[simp]
lemma map_apply_apply (hf : Injective f) (hg : Injective g) (r : α → β → Prop) (a : α) (b : β) :
    Relation.Map r f g (f a) (g b) ↔ r a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Injective f
hg : Injective g
r : α → β → Prop
a : α
b : β
⊢ Relation.Map r f g (f a) (g b) ↔ r a b

Tactic:
simp [Relation.Map, hf.eq_iff, hg.eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
    get? (m.insert k v) a = if k == a then some v else get? m a

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

Tactic:
simp_to_raw using Raw₀.Const.get?_insert

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]!

Proof state:
case cons
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast! = (head✝ :: tail✝)[(head✝ :: tail✝).length - 1]!

Tactic:
apply getLast!_of_getLast?

Result:
case cons.a
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast? = some (head✝ :: tail✝)[(head✝ :: tail✝).length - 1]!

Proof state:
case nil
α : Type u_1
inst✝ : Inhabited α
⊢ [].getLast! = [][[].length - 1]!

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
x : α
⊢ (head✝ :: tail✝).length - 1 = tail✝.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ l.getLast! = l[l.length - 1]!

Tactic:
cases l with
| nil => simp
| cons _ _ =>
  apply getLast!_of_getLast?
  rw [getElem!_pos, getElem_cons_length (h := by simp)]
  rfl

Result:
no goals

Proof state:
case cons.a
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast? = some ((head✝ :: tail✝).getLast ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
case cons.a
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast? = some (head✝ :: tail✝)[(head✝ :: tail✝).length - 1]!

Tactic:
rw [getElem!_pos, getElem_cons_length (h := by simp)]

Result:
case cons.a
α : Type u_1
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getLast? = some ((head✝ :: tail✝).getLast ⋯)
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
S : ι → Subring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma ι_descQ_eq_zero_of_boundary (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    h.ι ≫ h.descQ k (by rw [hx, S.zero_assoc, zero_comp]) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 0 = h.ι ≫ h.g' ≫ x

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0

Tactic:
rw [show 0 = h.ι ≫ h.g' ≫ x by simp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x

Tactic:
congr 1

Result:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.descQ k ⋯ = h.g' ≫ x

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.descQ k ⋯ = h.g' ≫ x

Tactic:
simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.11951, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.map_injective_iff (hf : Function.Injective f) :
    OrthogonalIdempotents (f ∘ e) ↔ OrthogonalIdempotents e

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective ⇑f
⊢ OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e

Tactic:
classical
simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective ⇑f
⊢ OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e

Tactic:
simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Result:
no goals
-- Mathlib/Algebra/Module/Rat.lean
theorem map_nnratCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [DivisionSemiring R] [DivisionSemiring S]
    [Module R M] [Module S M₂] (c : ℚ≥0) (x : M) :
    f ((c : R) • x) = (c : S) • f x

Proof state:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f (↑c • x) = ↑c • f x

Tactic:
rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
  map_natCast_smul f R S, map_inv_natCast_smul f R S]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_subset (x y : E × F) : segment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ [x-[𝕜]y] ⊆ [x.1-[𝕜]y.1] ×ˢ [x.2-[𝕜]y.2]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ [x.1-[𝕜]y.1] ×ˢ [x.2-[𝕜]y.2]

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ [x.1-[𝕜]y.1] ×ˢ [x.2-[𝕜]y.2]

Tactic:
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem edist_triangle : G.edist u w ≤ G.edist u v + G.edist v w

Proof state:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv

Result:
case inr.inr.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Proof state:
case inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
cases eq_or_ne (G.edist v w) ⊤ with
| inl hvw => simp [hvw]
| inr hvw =>
  obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
  obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
  rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
  exact edist_le _

Result:
no goals

Proof state:
case inl
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v = ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
simp [huv]

Result:
no goals

Proof state:
case inr.inl
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w = ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
simp [hvw]

Result:
no goals

Proof state:
case inr.inr.intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length

Tactic:
exact edist_le _

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v w : V
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
cases eq_or_ne (G.edist u v) ⊤ with
| inl huv => simp [huv]
| inr huv =>
  cases eq_or_ne (G.edist v w) ⊤ with
  | inl hvw => simp [hvw]
  | inr hvw =>
    obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
    obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
    rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
    exact edist_le _

Result:
no goals

Proof state:
case inr.inr.intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]

Result:
case inr.inr.intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length

Proof state:
case inr.inr.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw

Result:
case inr.inr.intro.intro
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ G.edist u v + G.edist v w
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_union_inter_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
    image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t :=
  coe_subset.1 <| by
    push_cast
    exact image2_union_inter_subset hf

Proof state:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∪ ↑t) (↑s ∩ ↑t) ⊆ image2 f ↑s ↑t

Tactic:
exact image2_union_inter_subset hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∪ t) (s ∩ t)) ⊆ ↑(image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∪ ↑t) (↑s ∩ ↑t) ⊆ image2 f ↑s ↑t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
    (f : { x // P x } → β) :
    (l.attachWith P H).map f =
      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩)

Proof state:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ map f ({ toList := toList✝ }.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) { toList := toList✝ } ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
P : α → Prop
H : ∀ (a : α), a ∈ l → P a
f : { x // P x } → β
⊢ map f (l.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) l ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ map f ({ toList := toList✝ }.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) { toList := toList✝ } ⋯
-- Mathlib/Tactic/NormNum/GCD.lean
theorem nat_lcm_helper (x y d m : ℕ) (hd : Nat.gcd x y = d)
    (d0 : Nat.beq d 0 = false)
    (dm : x * y = d * m) : Nat.lcm x y = m :=
  mul_right_injective₀ (Nat.ne_of_beq_eq_false d0) <| by
    dsimp only
    rw [← dm, ← hd, Nat.gcd_mul_lcm]

Proof state:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ (fun x => d * x) (x.lcm y) = (fun x => d * x) m

Tactic:
dsimp only

Result:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = d * m

Proof state:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = d * m

Tactic:
rw [← dm, ← hd, Nat.gcd_mul_lcm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_Iic_add_Ioi (h_left : IntegrableOn f (Iic b) μ)
    (h_right : IntegrableOn f (Ioi b) μ) :
    (∫ x in Iic b, f x ∂μ) + (∫ x in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ

Proof state:
case h.e'_3.h.e'_6
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
⊢ μ = μ.restrict (Iic b ∪ Ioi b)

Tactic:
rw [Iic_union_Ioi, Measure.restrict_univ]

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
convert (setIntegral_union (Iic_disjoint_Ioi <| Eq.le rfl) measurableSet_Ioi h_left h_right).symm

Result:
case h.e'_3.h.e'_6
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
⊢ μ = μ.restrict (Iic b ∪ Ioi b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.mul_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.mul p₂).denote ctx = p₁.denote ctx * p₂.denote ctx

Proof state:
ctx : Context
p₁✝ p₂ p₁ acc : Poly
⊢ denote ctx (mul.go p₂ [] acc) = denote ctx acc + denote ctx [] * denote ctx p₂

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx [] + denote ctx p₁ * denote ctx p₂ = denote ctx p₁ * denote ctx p₂

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
p₁✝ p₂ p₁ acc : Poly
⊢ denote ctx (mul.go p₂ p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂

Tactic:
match p₁ with
| [] => simp!
| (k, m) :: p₁ =>
  simp! [go p₁, Nat.left_distrib, add_denote, mulMon_denote,
         Nat.add_assoc, Nat.add_comm, Nat.add_left_comm,
         Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]

Result:
no goals

Proof state:
ctx : Context
p₁✝¹ p₂ p₁✝ acc : Poly
k : Nat
m : Mon
p₁ : List (Nat × Mon)
⊢ denote ctx (mul.go p₂ ((k, m) :: p₁) acc) = denote ctx acc + denote ctx ((k, m) :: p₁) * denote ctx p₂

Tactic:
simp! [go p₁, Nat.left_distrib, add_denote, mulMon_denote,
       Nat.add_assoc, Nat.add_comm, Nat.add_left_comm,
       Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]

Result:
no goals

Proof state:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx (p₁.mul p₂) = denote ctx p₁ * denote ctx p₂

Tactic:
simp [mul, go]

Result:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx [] + denote ctx p₁ * denote ctx p₂ = denote ctx p₁ * denote ctx p₂
-- Mathlib/RingTheory/Flat/Equalizer.lean
lemma Module.Flat.eqLocus_lTensor_eq [Module.Flat R M] :
    LinearMap.eqLocus (AlgebraTensorModule.lTensor S M f)
      (AlgebraTensorModule.lTensor S M g) =
      LinearMap.range (AlgebraTensorModule.lTensor S M (LinearMap.eqLocus f g).subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ LinearMap.eqLocus ((AlgebraTensorModule.lTensor S M) f) ((AlgebraTensorModule.lTensor S M) g) =
    LinearMap.range ((AlgebraTensorModule.lTensor S M) (LinearMap.eqLocus f g).subtype)

Tactic:
rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ LinearMap.ker ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g) =
    LinearMap.range ((AlgebraTensorModule.lTensor S M) (LinearMap.ker (f - g)).subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ LinearMap.ker ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g) =
    LinearMap.range ((AlgebraTensorModule.lTensor S M) (LinearMap.ker (f - g)).subtype)

Tactic:
rw [← map_sub, ker_lTensor_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma ι_φ : ι f g ≫ φ f g = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.lift (kernel.ι (f ≫ g)) (kernel.ι (f ≫ g) ≫ f) ≫ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) = 0

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ φ f g = 0

Tactic:
dsimp [ι, φ]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.lift (kernel.ι (f ≫ g)) (kernel.ι (f ≫ g) ≫ f) ≫ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ mapIdx f l = l.mapFinIdx fun i a x => f i a

Tactic:
simp [mapFinIdx_eq_mapIdx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ n, l₁.drop n <+ l₂.drop n
  | _, _, h, 0 => h
  | _, _, h, n + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop n

Proof state:
α : Type u_1
x✝¹ x✝ : List α
h : x✝¹ <+ x✝
n : Nat
⊢ drop (n + 1) x✝¹ <+ drop (n + 1) x✝

Tactic:
rw [← drop_tail, ← drop_tail]

Result:
α : Type u_1
x✝¹ x✝ : List α
h : x✝¹ <+ x✝
n : Nat
⊢ drop n x✝¹.tail <+ drop n x✝.tail

Proof state:
α : Type u_1
x✝¹ x✝ : List α
h : x✝¹ <+ x✝
n : Nat
⊢ drop n x✝¹.tail <+ drop n x✝.tail

Tactic:
exact h.tail.drop n

Result:
no goals