harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_isSome {a : α} : ∀ {l : List (Sigma β)}, (dlookup a l).isSome ↔ a ∈ l.keys
  | [] => by simp
  | ⟨a', b⟩ :: l => by
    by_cases h : a = a'
    · subst a'
      simp
    · simp [h, dlookup_isSome]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (dlookup a []).isSome = true ↔ a ∈ [].keys

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (dlookup a (⟨a, b⟩ :: l)).isSome = true ↔ a ∈ (⟨a, b⟩ :: l).keys

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (dlookup a (⟨a', b⟩ :: l)).isSome = true ↔ a ∈ (⟨a', b⟩ :: l).keys

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ (dlookup a (⟨a', b⟩ :: l)).isSome = true ↔ a ∈ (⟨a', b⟩ :: l).keys

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (dlookup a (⟨a', b⟩ :: l)).isSome = true ↔ a ∈ (⟨a', b⟩ :: l).keys

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ (dlookup a (⟨a', b⟩ :: l)).isSome = true ↔ a ∈ (⟨a', b⟩ :: l).keys

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (dlookup a (⟨a, b⟩ :: l)).isSome = true ↔ a ∈ (⟨a, b⟩ :: l).keys

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (dlookup a (⟨a', b⟩ :: l)).isSome = true ↔ a ∈ (⟨a', b⟩ :: l).keys

Tactic:
simp [h, dlookup_isSome]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_ne_top_iff_reachable : G.edist u v ≠ ⊤ ↔ G.Reachable u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.Walk u v → False
⊢ False

Tactic:
exact h.elim hx

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≠ ⊤ ↔ G.Reachable u v

Tactic:
refine ⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩

Result:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
⊢ G.edist u v ≠ ⊤

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
⊢ G.edist u v ≠ ⊤

Tactic:
by_contra hx

Result:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.edist u v = ⊤
⊢ False

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.edist u v = ⊤
⊢ False

Tactic:
simp only [edist, iInf_eq_top, ENat.coe_ne_top] at hx

Result:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.Walk u v → False
⊢ False
-- Mathlib/Analysis/Analytic/Basic.lean
lemma AnalyticWithinAt.congr_of_eventuallyEq_insert {f g : E → F} {s : Set E} {x : E}
    (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[insert x s] x] f) :
    AnalyticWithinAt 𝕜 g s x

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
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[insert x s] x] f
⊢ g x = f x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s) hs

Result:
no goals

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
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[insert x s] x] f
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs)

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
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[insert x s] x] f
⊢ g x = f x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem_eraseIdx (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : j < (l.eraseIdx i).size) :
    (l.eraseIdx i)[j] = if h'' : j < i then
        l[j]
      else
        l[j + 1]'(by rw [size_eraseIdx] at h'; omega)

Proof state:
α : Type ?u.47507
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < l.size - 1
h'' : ¬j < i
⊢ j + 1 < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.47507
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
h'' : ¬j < i
⊢ j + 1 < l.size

Tactic:
rw [size_eraseIdx] at h'

Result:
α : Type ?u.47507
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < l.size - 1
h'' : ¬j < i
⊢ j + 1 < l.size

Proof state:
case x
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
⊢ some (l.eraseIdx i h)[j] = some (if h'' : j < i then l[j] else l[j + 1])

Tactic:
rw [← getElem?_eq_getElem, getElem?_eraseIdx]

Result:
case x
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h'' : j < i then l[j] else l[j + 1])

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
⊢ (l.eraseIdx i h)[j] = if h'' : j < i then l[j] else l[j + 1]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
⊢ some (l.eraseIdx i h)[j] = some (if h'' : j < i then l[j] else l[j + 1])

Proof state:
case x
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < (l.eraseIdx i h).size
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h'' : j < i then l[j] else l[j + 1])

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraTower.lean
theorem Basis.smulTower_repr (x ij) :
    (b.smulTower c).repr x ij = b.repr (c.repr x ij.2) ij.1

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι × ι'
⊢ ((b.smulTower c).repr x) ij = (b.repr ((c.repr x) ij.2)) ij.1

Tactic:
simp [smulTower]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem Substructure.countable_fg_substructures_of_countable [Countable M] :
    Countable { S : L.Substructure M // S.FG }

Proof state:
case a
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ ↑S = ↑S'

Tactic:
rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]

Result:
case a
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ (closure L).toFun ↑(Exists.choose ⋯) = (closure L).toFun ↑(Exists.choose ⋯)

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ Countable { S // S.FG }

Tactic:
let g : { S : L.Substructure M // S.FG } → Finset M :=
  fun S ↦ Exists.choose S.prop

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
⊢ Countable { S // S.FG }

Proof state:
case a
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ (closure L).toFun ↑(Exists.choose ⋯) = (closure L).toFun ↑(Exists.choose ⋯)

Tactic:
exact congr_arg ((closure L) ∘ Finset.toSet) h

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
⊢ Function.Injective g

Tactic:
intro S S' h

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ S = S'

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
g_inj : Function.Injective g
⊢ Countable { S // S.FG }

Tactic:
exact Function.Embedding.countable ⟨g, g_inj⟩

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ S = S'

Tactic:
apply Subtype.eq

Result:
case a
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
S S' : { S // S.FG }
h : g S = g S'
⊢ ↑S = ↑S'

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
⊢ Countable { S // S.FG }

Tactic:
have g_inj : Function.Injective g := by
  intro S S' h
  apply Subtype.eq
  rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]
  exact congr_arg ((closure L) ∘ Finset.toSet) h

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S => Exists.choose ⋯
g_inj : Function.Injective g
⊢ Countable { S // S.FG }
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_uIoc_iff [LinearOrder α] {a b : α} {P : α → Prop} :
    (∀ᵐ x ∂μ.restrict (Ι a b), P x) ↔
      (∀ᵐ x ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ x ∂μ.restrict (Ioc b a), P x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x

Tactic:
rw [ae_restrict_uIoc_eq, eventually_sup]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_range {α} [Small.{u} α] (f : α → ZFSet.{u}) :
    (range f).toSet = Set.range f

Proof state:
case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x✝ : ZFSet.{u}
⊢ x✝ ∈ (range f).toSet ↔ x✝ ∈ Set.range f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).toSet = Set.range f

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x✝ : ZFSet.{u}
⊢ x✝ ∈ (range f).toSet ↔ x✝ ∈ Set.range f
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :
    4 ^ n ≤ (2 * n + 1) * (2 * n).choose n :=
  calc
    4 ^ n = (1 + 1) ^ (2 * n)

Proof state:
n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)

Tactic:
norm_num [pow_mul]

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) = (2 * n + 1) * (2 * n).choose n

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ m ∈ range (2 * n + 1), (2 * n).choose m ≤ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2)

Tactic:
gcongr

Result:
case h
n i✝ : ℕ
a✝ : i✝ ∈ range (2 * n + 1)
⊢ (2 * n).choose i✝ ≤ (2 * n).choose (2 * n / 2)

Proof state:
case h
n i✝ : ℕ
a✝ : i✝ ∈ range (2 * n + 1)
⊢ (2 * n).choose i✝ ≤ (2 * n).choose (2 * n / 2)

Tactic:
apply choose_le_middle

Result:
no goals

Proof state:
n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m

Tactic:
simp [add_pow]

Result:
no goals

Proof state:
n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m

Tactic:
set_option simprocs false in simp [add_pow]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma smul_comp {n₁ n₂ n₁₂ : ℤ} (k : R) (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (k • z₁).comp z₂ h = k • (z₁.comp z₂ h)

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((k • z₁).comp z₂ h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), smul_v, Linear.smul_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (k • z₁).comp z₂ h = k • z₁.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((k • z₁).comp z₂ h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem length_pos_of_prod_ne_one (L : List M) (h : L.prod ≠ 1) : 0 < L.length

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
simp

Result:
no goals

Proof state:
case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

Tactic:
simp at h

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
L : List M
h : L.prod ≠ 1
⊢ 0 < L.length

Tactic:
cases L

Result:
case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.to_average {f : α → β} (h : Integrable f μ) : Integrable f ((μ univ)⁻¹ • μ)

Proof state:
case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
hne : μ ≠ 0
⊢ Integrable f ((μ univ)⁻¹ • μ)

Tactic:
apply h.smul_measure

Result:
case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
hne : μ ≠ 0
⊢ (μ univ)⁻¹ ≠ ⊤

Proof state:
case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f 0
⊢ Integrable f ((0 univ)⁻¹ • 0)

Tactic:
rwa [smul_zero]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
hne : μ ≠ 0
⊢ (μ univ)⁻¹ ≠ ⊤

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
⊢ Integrable f ((μ univ)⁻¹ • μ)

Tactic:
rcases eq_or_ne μ 0 with (rfl | hne)

Result:
case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f 0
⊢ Integrable f ((0 univ)⁻¹ • 0)

case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
hne : μ ≠ 0
⊢ Integrable f ((μ univ)⁻¹ • μ)
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem toTrivSqZeroExt_comp_map [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module Rᵐᵒᵖ N]
    [IsCentralScalar R N] (f : M →ₗ[R] N) :
    toTrivSqZeroExt.comp (map f) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt

Proof state:
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ toTrivSqZeroExt.comp (map f) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt

Tactic:
apply hom_ext

Result:
case h
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ (toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R = ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R

Proof state:
case h
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ (toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R = ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R

Tactic:
apply LinearMap.ext

Result:
case h.h
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ ∀ (x : M),
    ((toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R) x =
      (((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R) x

Proof state:
case h.h
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ ∀ (x : M),
    ((toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R) x =
      (((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R) x

Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
  AlgHom.toLinearMap_apply, map_apply_ι, toTrivSqZeroExt_ι, TrivSqZeroExt.map_inr, forall_const]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_prod_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → I ⊔ J i = ⊤) :
    (I ⊔ ∏ i ∈ s, J i) = ⊤ :=
  Finset.prod_induction _ (fun J => I ⊔ J = ⊤)
    (fun _ _ hJ hK => (sup_mul_eq_of_coprime_left hJ).trans hK)
    (by simp_rw [one_eq_top, sup_top_eq]) h

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ (fun J => I ⊔ J = ⊤) 1

Tactic:
simp_rw [one_eq_top, sup_top_eq]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma respectsIso :
    RespectsIso FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
this : Algebra R S := e.toRingHom.toAlgebra
⊢ e.toRingHom.FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective

Result:
no goals

Proof state:
⊢ ∀ {R S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
intros R S _ _ e

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FormallyUnramified

Tactic:
letI := e.toRingHom.toAlgebra

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
this : Algebra R S := e.toRingHom.toAlgebra
⊢ e.toRingHom.FormallyUnramified

Proof state:
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] => FormallyUnramified

Tactic:
refine stableUnderComposition.respectsIso ?_

Result:
⊢ ∀ {R S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_μ_zero_app (m₁ m₂ : M) (X : C) [F.Monoidal]:
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫ (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫
    (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
    (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)

Tactic:
rw [← obj_η_app_assoc, ← Functor.map_comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (F.obj m₂).map ((η F).app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (F.obj m₂).map ((η F).app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inr_desc : inr φ ≫ desc φ α β eq = β

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ inr φ ≫ desc φ α β eq = β

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0

Proof state:
i j : ℤ
⊢ i.gcd j = 0 ↔ i = 0 ∧ j = 0

Tactic:
rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.orderOf (hf : IsCycle f) : orderOf f = #f.support

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ Fintype.card ↥(Subgroup.zpowers f) = Fintype.card { x // x ∈ f.support }

Tactic:
convert Fintype.card_congr (IsCycle.zpowersEquivSupport hf)

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ orderOf f = #f.support

Tactic:
rw [← Fintype.card_zpowers, ← Fintype.card_coe]

Result:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ Fintype.card ↥(Subgroup.zpowers f) = Fintype.card { x // x ∈ f.support }
-- Mathlib/Algebra/Group/ForwardDiff.lean
@[simp] lemma fwdDiff_iter_finset_sum {α : Type*} (s : Finset α) (f : α → M → G) (n : ℕ) :
    Δ_[h]^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, Δ_[h]^[n] (f k)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
α : Type u_3
s : Finset α
f : α → M → G
n : ℕ
⊢ Δ_[h]^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, Δ_[h]^[n] (f k)

Tactic:
simpa only [coe_fwdDiffₗ_pow] using map_sum (fwdDiffₗ M G h ^ n) f s

Result:
no goals
-- Mathlib/RingTheory/RingHom/Flat.lean
/-- Composition of flat ring homomorphisms is flat. -/
lemma comp {f : R →+* S} {g : S →+* T} (hf : f.Flat) (hg : g.Flat) : Flat (g.comp f)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Tactic:
algebraize [f, g, (g.comp f)]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Flat R S
algebraizeInst✝ : Module.Flat S T
⊢ (g.comp f).Flat

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Flat R S
algebraizeInst✝ : Module.Flat S T
⊢ (g.comp f).Flat

Tactic:
exact Module.Flat.trans R S T

Result:
no goals