harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma IsValuedIn.trans (T : Type*) [CommRing T] [Algebra T S] [Algebra T R] [IsScalarTower T S R]
    [P.IsValuedIn T] :
    P.IsValuedIn S where
  exists_value i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
T : Type u_6
inst✝⁴ : CommRing T
inst✝³ : Algebra T S
inst✝² : Algebra T R
inst✝¹ : IsScalarTower T S R
inst✝ : P.IsValuedIn T
i j : ι
⊢ ∃ s, (algebraMap S R) s = P.pairing i j

Tactic:
use algebraMap T S (P.pairingIn T i j)

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
T : Type u_6
inst✝⁴ : CommRing T
inst✝³ : Algebra T S
inst✝² : Algebra T R
inst✝¹ : IsScalarTower T S R
inst✝ : P.IsValuedIn T
i j : ι
⊢ (algebraMap S R) ((algebraMap T S) (P.pairingIn T i j)) = P.pairing i j

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
T : Type u_6
inst✝⁴ : CommRing T
inst✝³ : Algebra T S
inst✝² : Algebra T R
inst✝¹ : IsScalarTower T S R
inst✝ : P.IsValuedIn T
i j : ι
⊢ (algebraMap S R) ((algebraMap T S) (P.pairingIn T i j)) = P.pairing i j

Tactic:
simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem BilinForm.toMatrix_basisFun :
    BilinForm.toMatrix (Pi.basisFun R₁ n) = BilinForm.toMatrix'

Proof state:
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ toMatrix (Pi.basisFun R₁ n) = BilinForm.toMatrix'

Tactic:
rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem modify_of_valid (cs cs' : List Char) :
    modify ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ f = ⟨cs ++ cs'.modifyHead f⟩

Proof state:
f : Char → Char
cs cs' : List Char
⊢ { data := cs ++ cs' }.modify { byteIdx := utf8Len cs } f = { data := cs ++ List.modifyHead f cs' }

Tactic:
rw [modify, set_of_valid, get_of_valid]

Result:
f : Char → Char
cs cs' : List Char
⊢ { data := cs ++ List.modifyHead (fun x => f (cs'.headD default)) cs' } = { data := cs ++ List.modifyHead f cs' }

Proof state:
f : Char → Char
cs cs' : List Char
⊢ { data := cs ++ List.modifyHead (fun x => f (cs'.headD default)) cs' } = { data := cs ++ List.modifyHead f cs' }

Tactic:
cases cs' <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- If `p` is a prime and `n` is `p`-smooth, then `p` and `n` are coprime. -/
lemma Prime.smoothNumbers_coprime {p n : ℕ} (hp : p.Prime) (hn : n ∈ smoothNumbers p) :
    Nat.Coprime p n

Proof state:
p n : ℕ
hp : Prime p
hn : n ∈ p.smoothNumbers
⊢ p.Coprime n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers] at hn

Result:
p n : ℕ
hp : Prime p
hn : n ∈ factoredNumbers (Finset.range p)
⊢ p.Coprime n

Proof state:
p n : ℕ
hp : Prime p
hn : n ∈ factoredNumbers (Finset.range p)
⊢ p.Coprime n

Tactic:
exact hp.factoredNumbers_coprime Finset.not_mem_range_self hn

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem le_pi_iff {I : Set η} {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    J ≤ pi I H ↔ ∀ i : η, i ∈ I → map (Pi.evalMonoidHom f i) J ≤ H i

Proof state:
case mp.intro.intro
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
x : (i : η) → f i
hx : x ∈ ↑J
⊢ (Pi.evalMonoidHom f i) x ∈ H i

Tactic:
exact (h hx) _ hi

Result:
no goals

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H ↔ ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i

Tactic:
constructor

Result:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H → ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i

case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i) → J ≤ pi I H

Proof state:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi I H → ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i

Tactic:
intro h i hi

Result:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
⊢ map (Pi.evalMonoidHom f i) J ≤ H i

Proof state:
case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i
x : (i : η) → f i
hx : x ∈ J
i : η
hi : i ∈ I
⊢ x i ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) i

Tactic:
exact h i hi ⟨_, hx, rfl⟩

Result:
no goals

Proof state:
case mp
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
⊢ map (Pi.evalMonoidHom f i) J ≤ H i

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case mp.intro.intro
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : J ≤ pi I H
i : η
hi : i ∈ I
x : (i : η) → f i
hx : x ∈ ↑J
⊢ (Pi.evalMonoidHom f i) x ∈ H i

Proof state:
case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i) → J ≤ pi I H

Tactic:
intro h x hx i hi

Result:
case mpr
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i
x : (i : η) → f i
hx : x ∈ J
i : η
hi : i ∈ I
⊢ x i ∈ (fun i => ((fun i => (H i).toSubmonoid) i).carrier) i
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem comp_ι_eq : f.comp (ι f g) = g.comp (ι f g)

Proof state:
case H
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f.comp (ι f g)) x = (g.comp (ι f g)) x

Tactic:
rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]

Result:
case H
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f - g) ((ι f g) x) = 0

Proof state:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
⊢ f.comp (ι f g) = g.comp (ι f g)

Tactic:
ext x

Result:
case H
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f.comp (ι f g)) x = (g.comp (ι f g)) x

Proof state:
case H
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f - g) ((ι f g) x) = 0

Tactic:
exact x.2

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
@[to_additive]
lemma eq_mul_of_ne_all {x y z : G} (hx : x ≠ 1)
    (hy : y ≠ 1) (hxy : x ≠ y) (hz : z ≠ 1) (hzx : z ≠ x) (hzy : z ≠ y) : z = x * y

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
x✝ : Fintype G := Fintype.ofFinite G
⊢ z = x * y

Tactic:
apply eq_of_mem_insert_of_not_mem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
x✝ : Fintype G := Fintype.ofFinite G
⊢ z ∉ {x, y, 1}

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
⊢ z = x * y

Tactic:
classical
let _ := Fintype.ofFinite G
apply eq_of_mem_insert_of_not_mem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _
simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
x✝ : Fintype G := Fintype.ofFinite G
⊢ z ∉ {x, y, 1}

Tactic:
simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
⊢ z = x * y

Tactic:
let _ := Fintype.ofFinite G

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
x✝ : Fintype G := Fintype.ofFinite G
⊢ z = x * y
-- Mathlib/ModelTheory/Basic.lean
theorem comp_right_injective (h : M ≃[L] N) :
    Function.Injective (fun f ↦ f.comp h : (N ≃[L] P) → (M ≃[L] P))

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
⊢ Function.Injective fun f => f.comp h

Tactic:
intro f g hfg

Result:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f => f.comp h) f = (fun f => f.comp h) g
⊢ f = g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f => f.comp h) f = (fun f => f.comp h) g
⊢ f = g

Tactic:
convert (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg) <;>
  rw [comp_assoc, self_comp_symm, comp_refl]

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem self_act_invAct_eq {x y : R} : (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rw [← left_cancel (x ◃ x)]

Result:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = x ◃ x ◃⁻¹ y

Tactic:
rw [right_inv]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y

Tactic:
rw [right_inv]

Result:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y

Tactic:
rw [self_act_act_eq]

Result:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = x ◃ x ◃⁻¹ y
-- Mathlib/Algebra/Algebra/Equiv.lean
theorem symm_comp (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁

Proof state:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e.symm).comp ↑e = AlgHom.id R A₁

Tactic:
ext

Result:
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₁
⊢ ((↑e.symm).comp ↑e) x✝ = (AlgHom.id R A₁) x✝

Proof state:
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₁
⊢ ((↑e.symm).comp ↑e) x✝ = (AlgHom.id R A₁) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@[simp]
lemma deriv_mul_log {x : ℝ} (hx : x ≠ 0) : deriv (fun x ↦ x * log x) x = log x + 1

Proof state:
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x) x * log x + x * deriv log x = log x + 1

Tactic:
simp only [deriv_id'', one_mul, deriv_log', ne_eq, add_right_inj]

Result:
x : ℝ
hx : x ≠ 0
⊢ x * x⁻¹ = 1

Proof state:
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x * log x) x = log x + 1

Tactic:
rw [deriv_mul differentiableAt_id' (differentiableAt_log hx)]

Result:
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x) x * log x + x * deriv log x = log x + 1

Proof state:
x : ℝ
hx : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ hx

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma _root_.SymmetricRel.dynEntourage (T : X → X) {U : Set (X × X)} (h : SymmetricRel U) (n : ℕ) :
    SymmetricRel (dynEntourage T U n)

Proof state:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
⊢ xy ∈ swap ⁻¹' Dynamics.dynEntourage T U n ↔ xy ∈ Dynamics.dynEntourage T U n

Tactic:
simp only [Dynamics.dynEntourage, map_iterate, mem_preimage, mem_iInter]

Result:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
⊢ (∀ i < n, map T^[i] T^[i] xy.swap ∈ U) ↔ ∀ i < n, map T^[i] T^[i] xy ∈ U

Proof state:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
⊢ (∀ i < n, map T^[i] T^[i] xy.swap ∈ U) ↔ ∀ i < n, map T^[i] T^[i] xy ∈ U

Tactic:
refine forall₂_congr fun k _ ↦ ?_

Result:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
k : ℕ
x✝ : k < n
⊢ map T^[k] T^[k] xy.swap ∈ U ↔ map T^[k] T^[k] xy ∈ U

Proof state:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
k : ℕ
x✝ : k < n
⊢ map T^[k] T^[k] xy.swap ∈ U ↔ map T^[k] T^[k] xy ∈ U

Tactic:
exact map_apply' _ _ _ ▸ SymmetricRel.mk_mem_comm h

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
⊢ SymmetricRel (Dynamics.dynEntourage T U n)

Tactic:
ext xy

Result:
case h
X : Type u_1
T : X → X
U : Set (X × X)
h : SymmetricRel U
n : ℕ
xy : X × X
⊢ xy ∈ swap ⁻¹' Dynamics.dynEntourage T U n ↔ xy ∈ Dynamics.dynEntourage T U n
-- Mathlib/Data/Nat/GCD/Basic.lean
lemma add_coprime_iff_right (h : c ∣ a) : Coprime (a + b) c ↔ Coprime b c

Proof state:
case intro
b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℕ
h : c ∣ a
⊢ (a + b).Coprime c ↔ b.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c
-- Mathlib/Data/DFinsupp/Defs.lean
theorem update_eq_erase_add_single {β : ι → Type*} [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i)
    (i : ι) (b : β i) : f.update i b = f.erase i + single i b

Proof state:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = erase i f + single i b

Tactic:
ext j

Result:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (erase i f + single i b) j

Proof state:
case h
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (erase i f + single i b) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Result:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (erase i f + single i b) i

case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (erase i f + single i b) j

Proof state:
case h.inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (erase i f + single i b) i

Tactic:
simp

Result:
no goals

Proof state:
case h.inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (erase i f + single i b) j

Tactic:
simp [Function.update_of_ne h.symm, h, erase_ne, h.symm]

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem delayReflRight_one (γ : Path x y) : delayReflRight 1 γ = γ

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ (delayReflRight 1 γ) t = γ t

Tactic:
exact congr_arg γ (qRight_one_right t)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 1 γ = γ

Tactic:
ext t

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ (delayReflRight 1 γ) t = γ t
-- Mathlib/GroupTheory/Index.lean
theorem relindex_sup_left [K.Normal] : K.relindex (K ⊔ H) = K.relindex H

Proof state:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : K.Normal
⊢ K.relindex (K ⊔ H) = K.relindex H

Tactic:
rw [sup_comm, relindex_sup_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp]
lemma isFinitelySemisimple_iff_isSemisimple [Module.Finite R M] :
    f.IsFinitelySemisimple ↔ f.IsSemisimple

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
⊢ f.IsFinitelySemisimple ↔ f.IsSemisimple

Tactic:
refine ⟨fun hf ↦ isSemisimple_iff.mpr fun p hp ↦ ?_, IsSemisimple.isFinitelySemisimple⟩

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq₁ : q ∈ f.invtSubmodule
hq₂ : Disjoint p q
hq₃ : p ⊔ q = ⊤
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
exact ⟨q, hq₁, hq₂, codisjoint_iff.mpr hq₃⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
obtain ⟨q, -, hq₁, hq₂, hq₃⟩ :=
  isFinitelySemisimple_iff.mp hf ⊤ (invtSubmodule.top_mem f) inferInstance p hp le_top

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq₁ : q ∈ f.invtSubmodule
hq₂ : Disjoint p q
hq₃ : p ⊔ q = ⊤
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Function.Embedding.toEquivRange_symm_apply_self (a : α) :
    f.toEquivRange.symm ⟨f a, Set.mem_range_self a⟩ = a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
a : α
⊢ f.toEquivRange.symm ⟨f a, ⋯⟩ = a

Tactic:
simp [Equiv.symm_apply_eq]

Result:
no goals
-- Mathlib/Algebra/GradedMonoid.lean
theorem List.dProd_monoid {α} [AddMonoid ι] [Monoid R] (l : List α) (fι : α → ι) (fA : α → R) :
    @List.dProd _ _ (fun _ : ι => R) _ _ l fι fA = (l.map fA).prod

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ [].dProd fι fA = (map fA []).prod

Tactic:
rw [List.dProd_nil, List.map_nil, List.prod_nil]

Result:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ GradedMonoid.GOne.one = 1

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ GradedMonoid.GOne.one = 1

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ (head :: tail).dProd fι fA = (map fA (head :: tail)).prod

Tactic:
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]

Result:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (map fA tail).prod = fA head * (map fA tail).prod

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ l.dProd fι fA = (map fA l).prod

Tactic:
match l with
| [] =>
  rw [List.dProd_nil, List.map_nil, List.prod_nil]
  rfl
| head::tail =>
  rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
  rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (map fA tail).prod = fA head * (map fA tail).prod

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.sup_principal (hl : l.HasBasis p s) (t : Set α) :
    (l ⊔ 𝓟 t).HasBasis p fun i => s i ∪ t :=
  ⟨fun u => by
    simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, exists_prop, and_true,
      Unique.exists_iff]⟩

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t u : Set α
⊢ u ∈ l ⊔ 𝓟 t ↔ ∃ i, p i ∧ s i ∪ t ⊆ u

Tactic:
simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, exists_prop, and_true,
  Unique.exists_iff]

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
lemma monotone_isoClosure (h : P ≤ Q) : isoClosure P ≤ isoClosure Q

Proof state:
case intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Q.isoClosure X

Tactic:
exact ⟨X', h _ hX', ⟨e⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
rintro X ⟨X', hX', ⟨e⟩⟩

Result:
case intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Q.isoClosure X
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma map_comp_isoH1_hom :
    map f φ 1 ≫ (isoH1 B).hom = (isoH1 A).hom ≫ H1Map f φ

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
⊢ map f φ 1 ≫ (isoH1 B).hom = (isoH1 A).hom ≫ H1Map f φ

Tactic:
simp [← cancel_epi (groupCohomologyπ _ _), H1Map, Category.assoc]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem inf_neBot_iff_frequently_left {f g : Filter α} :
    NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x

Proof state:
α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

Tactic:
simp only [inf_neBot_iff, frequently_iff, and_comm]

Result:
α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U