harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem Filter.EventuallyEq.of_mulIndicator [One β] {l : Filter α} {f : α → β}
    (hf : ∀ᶠ x in l, f x ≠ 1) {s t : Set α} (h : s.mulIndicator f =ᶠ[l] t.mulIndicator f) :
    s =ᶠ[l] t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
⊢ s =ᶠ[l] t

Tactic:
have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦ by
  rw [mulSupport_mulIndicator]
  exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq

Result:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
⊢ s =ᶠ[l] t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
rw [mulSupport_mulIndicator]

Result:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s

Tactic:
exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
⊢ s =ᶠ[l] t

Tactic:
exact this.symm.trans <| h.mulSupport.trans this

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem mono_iff_injective {X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f

Proof state:
X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective f

Tactic:
constructor

Result:
case mp
X Y : Type u
f : X ⟶ Y
⊢ Mono f → Function.Injective f

case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Injective f → Mono f

Proof state:
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Injective f → Mono f

Tactic:
exact fun H => ⟨fun g g' h => H.comp_left h⟩

Result:
no goals

Proof state:
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'

Tactic:
exact (cancel_mono f).mp h

Result:
no goals

Proof state:
case mp
X Y : Type u
f : X ⟶ Y
⊢ Mono f → Function.Injective f

Tactic:
intro H x x' h

Result:
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'

Proof state:
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'

Tactic:
rw [← homOfElement_eq_iff] at h ⊢

Result:
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_mkVector {n : Nat} {a : α} {b : β} :
    unzip (mkVector n (a, b)) = (mkVector n a, mkVector n b)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
a : α
b : β
⊢ (mkVector n (a, b)).unzip = (mkVector n a, mkVector n b)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_self_iff_indep : M.IsBasis I I ↔ M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.IsBasis I I ↔ M.Indep I

Tactic:
rw [isBasis_iff', and_iff_right rfl.subset, and_assoc, and_iff_left_iff_imp]

Result:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ I → I = J) ∧ I ⊆ M.E

Tactic:
exact fun hi ↦ ⟨fun _ _ ↦ subset_antisymm, hi.subset_ground⟩

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.measure_eq_zero_or_one_of_indepSet_self' (h : ∀ᵐ a ∂μα, IsFiniteMeasure (κ a))
    {t : Set Ω} (h_indep : IndepSet t t κ μα) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
filter_upwards [measure_eq_zero_or_one_or_top_of_indepSet_self h_indep, h] with a h_0_1_top h'

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
h' : IsFiniteMeasure (κ a)
⊢ (κ a) t = 0 ∨ (κ a) t = 1

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
h' : IsFiniteMeasure (κ a)
⊢ (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
simpa only [measure_ne_top (κ a), or_false] using h_0_1_top

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
@[simp] lemma count_ne_zero'' [Nonempty α] : (count : Measure α) ≠ 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
⊢ count ≠ 0

Tactic:
simp [count]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFreeOn.mono (hmn : m ≤ n) (hG : G.CliqueFreeOn s m) : G.CliqueFreeOn s n

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
⊢ G.CliqueFreeOn s n

Tactic:
rintro t hts ht

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : ↑t ⊆ s
ht : G.IsNClique n t
⊢ False

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : ↑t ⊆ s
ht : G.IsNClique n t
u : Finset α
hut : u ⊆ t
hu : #u = m
⊢ False

Tactic:
exact hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : ↑t ⊆ s
ht : G.IsNClique n t
⊢ False

Tactic:
obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : ↑t ⊆ s
ht : G.IsNClique n t
u : Finset α
hut : u ⊆ t
hu : #u = m
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ k = k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ (ofList l).get k' h = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.get_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
/-- The diagonal of a formally unramified morphism of finite type is an open immersion. -/
lemma AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [FormallyUnramified f] [LocallyOfFiniteType f] : IsOpenImmersion (pullback.diagonal f)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
i : (Scheme.Cover.pullbackCover 𝒰Y f).J
j : (𝒰X i).J
hu : FormallyUnramified ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)))

Tactic:
have hfin : LocallyOfFiniteType ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)) :=
  comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
i : (Scheme.Cover.pullbackCover 𝒰Y f).J
j : (𝒰X i).J
hu : FormallyUnramified ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i))
hfin : LocallyOfFiniteType ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)))
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma leftHomologyIso_inv_naturality :
    S₁.leftHomologyIso.inv ≫ leftHomologyMap φ =
      homologyMap φ ≫ S₂.leftHomologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = homologyMap φ ≫ S₂.leftHomologyIso.inv

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using
  LeftHomologyData.leftHomologyIso_hom_naturality φ S₁.leftHomologyData S₂.leftHomologyData

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_hom_comp_d (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) :
    (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃
-- Mathlib/Data/Fintype/EquivFin.lean
theorem toEmbedding_equivOfFiniteSelfEmbedding [Finite α] (e : α ↪ α) :
    e.equivOfFiniteSelfEmbedding.toEmbedding = e

Proof state:
case h
α : Type u_1
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding x✝ = e x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
e : α ↪ α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding x✝ = e x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem isPrefix_aig (aig : AIG α) (input : β aig) :
    IsPrefix aig.decls (f aig input).aig.decls

Proof state:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]

Tactic:
apply decl_eq

Result:
no goals

Proof state:
case size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
apply le_size

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ IsPrefix aig.decls (f aig input).aig.decls

Tactic:
apply IsPrefix.of

Result:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Proof state:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

Tactic:
intro idx h

Result:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem hasSum_log_one_add {a : ℝ} (h : 0 ≤ a) :
    HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * (a / (a + 2)) ^ (2 * k + 1))
      (log (1 + a))

Proof state:
a : ℝ
h : 0 ≤ a
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
obtain (rfl | ha0) := eq_or_ne a 0

Result:
case inl
h : 0 ≤ 0
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (0 / (0 + 2)) ^ (2 * k + 1)) (log (1 + 0))

case inr
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Proof state:
case inl
h : 0 ≤ 0
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (0 / (0 + 2)) ^ (2 * k + 1)) (log (1 + 0))

Tactic:
simp [hasSum_zero]

Result:
no goals

Proof state:
case h.e'_5.h.h.e'_6.h.e'_5
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
x✝ : ℕ
⊢ a / (a + 2) = 1 / (2 * a⁻¹ + 1)

case h.e'_6.h.e'_1.h.e'_6
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ a = a⁻¹⁻¹

Tactic:
all_goals field_simp [add_comm]

Result:
no goals

Proof state:
case h.e'_6.h.e'_1.h.e'_6
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ a = a⁻¹⁻¹

Tactic:
field_simp [add_comm]

Result:
no goals

Proof state:
case inr
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
convert hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4

Result:
case h.e'_5.h.h.e'_6.h.e'_5
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
x✝ : ℕ
⊢ a / (a + 2) = 1 / (2 * a⁻¹ + 1)

case h.e'_6.h.e'_1.h.e'_6
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ a = a⁻¹⁻¹
-- Mathlib/Data/Finsupp/Single.lean
theorem single_apply [Decidable (a = a')] : single a b a' = if a = a' then b else 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
classical
simp_rw [@eq_comm _ a a']
convert Pi.single_apply a b a'

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a' = a then b else 0

Tactic:
convert Pi.single_apply a b a'

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
simp_rw [@eq_comm _ a a']

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a' = a then b else 0
-- Mathlib/Data/Finset/Fold.lean
theorem fold_insert [DecidableEq α] (h : a ∉ s) :
    (insert a s).fold op b f = f a * s.fold op b f

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
unfold fold

Result:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
rw [insert_val, ndinsert_of_not_mem h, Multiset.map_cons, fold_cons_left]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Polynomial.lean
lemma KaehlerDifferential.mvPolynomialBasis_repr_symm_single (σ) (i) (x) :
    (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • D R (MvPolynomial σ R) (.X i)

Proof state:
case a
R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
⊢ (mvPolynomialBasis R σ).repr ((mvPolynomialBasis R σ).repr.symm (Finsupp.single i x)) =
    (mvPolynomialBasis R σ).repr (x • (D R (MvPolynomial σ R)) (MvPolynomial.X i))

Tactic:
simp [LinearEquiv.map_smul, -map_smul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
⊢ (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (D R (MvPolynomial σ R)) (MvPolynomial.X i)

Tactic:
apply (mvPolynomialBasis R σ).repr.injective

Result:
case a
R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
⊢ (mvPolynomialBasis R σ).repr ((mvPolynomialBasis R σ).repr.symm (Finsupp.single i x)) =
    (mvPolynomialBasis R σ).repr (x • (D R (MvPolynomial σ R)) (MvPolynomial.X i))
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_f_2_comp_twoCochainsLequiv :
    (cochainsMap f φ).f 2 ≫ (twoCochainsLequiv B).toModuleIso.hom =
      (twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fTwo f φ)

Proof state:
case hf.h.h.h.e_6.h.e_a.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x✝ : ↑((inhomogeneousCochains A).X 2)
g : G × G
x : Fin 2
⊢ (fun x => ⇑f ∘ x) ((piFinTwoEquiv fun x => G).symm g) x = (piFinTwoEquiv fun x => H).symm (Prod.map (⇑f) (⇑f) g) x

Tactic:
fin_cases x <;> rfl

Result:
no goals

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (ConcreteCategory.hom φ.hom) (x ((fun x => ⇑f ∘ x) ((piFinTwoEquiv fun x => G).symm g))) =
    (ConcreteCategory.hom φ.hom) (x ((piFinTwoEquiv fun x => H).symm (Prod.map (⇑f) (⇑f) g)))

Tactic:
rcongr x

Result:
case hf.h.h.h.e_6.h.e_a.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x✝ : ↑((inhomogeneousCochains A).X 2)
g : G × G
x : Fin 2
⊢ (fun x => ⇑f ∘ x) ((piFinTwoEquiv fun x => G).symm g) x = (piFinTwoEquiv fun x => H).symm (Prod.map (⇑f) (⇑f) g) x

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cochainsMap f φ).f 2 ≫ (twoCochainsLequiv B).toModuleIso.hom =
    (twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fTwo f φ)

Tactic:
ext x g

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (twoCochainsLequiv B).toModuleIso.hom)) x g =
    (ModuleCat.Hom.hom ((twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fTwo f φ))) x g

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (twoCochainsLequiv B).toModuleIso.hom)) x g =
    (ModuleCat.Hom.hom ((twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fTwo f φ))) x g

Tactic:
show φ.hom (x _) = φ.hom (x _)

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (ConcreteCategory.hom φ.hom) (x ((fun x => ⇑f ∘ x) ((piFinTwoEquiv fun x => G).symm g))) =
    (ConcreteCategory.hom φ.hom) (x ((piFinTwoEquiv fun x => H).symm (Prod.map (⇑f) (⇑f) g)))