harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lieModule_lcs_map_le (k : ℕ) :
    (lowerCentralSeries R L M k : Submodule R M).map g ≤ lowerCentralSeries R L₂ M₂ k

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ ⇑g '' {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} ⊆ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))

Tactic:
rintro m₂ ⟨m, ⟨x, n, m_n, ⟨h₁, h₂⟩⟩, rfl⟩

Result:
case succ.intro.intro.intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
m : M
x : L
n : x ∈ ⊤
m_n : M
h₁ : m_n ∈ lowerCentralSeries R L M k
h₂ : ⁅x, m_n⁆ = m
⊢ g m ∈ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_rpow_le_add {p : ℝ} (a b : ℝ≥0) (hp1 : 1 ≤ p) :
    (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Proof state:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < p⁻¹

Tactic:
simp [lt_of_lt_of_le zero_lt_one hp1]

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
rw [one_div]

Result:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ p⁻¹ ≤ a + b

Proof state:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
exact add_rpow_le_rpow_add _ _ hp1

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹

Tactic:
rw [inv_inv]

Result:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ p⁻¹ ≤ a + b

Tactic:
rw [← @NNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]

Result:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
lemma exp_add (x y : EReal) : exp (x + y) = exp x * exp y

Proof state:
case h_top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
induction y

Result:
case h_top.h_bot

⊢ (⊤ + ⊥).exp = ⊤.exp * ⊥.exp

case h_top.h_real
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

case h_top.h_top

⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

Tactic:
simp only [← EReal.coe_add, exp_coe]

Result:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp (a✝¹ + a✝)) = ENNReal.ofReal (Real.exp a✝¹) * ENNReal.ofReal (Real.exp a✝)

Proof state:
case h_top.h_real
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

Tactic:
simp only [EReal.top_add_coe, exp_top, exp_coe]

Result:
case h_top.h_real
a✝ : ℝ
⊢ ⊤ = ⊤ * ENNReal.ofReal (Real.exp a✝)

Proof state:
case h_real.h_top
a✝ : ℝ
⊢ ⊤ = ENNReal.ofReal (Real.exp a✝) * ⊤

Tactic:
rw [ENNReal.mul_top]

Result:
case h_real.h_top
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Proof state:
case h_real.h_top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Tactic:
simp only [EReal.coe_add_top, exp_top, exp_coe]

Result:
case h_real.h_top
a✝ : ℝ
⊢ ⊤ = ENNReal.ofReal (Real.exp a✝) * ⊤

Proof state:
x y : EReal
⊢ (x + y).exp = x.exp * y.exp

Tactic:
induction x

Result:
case h_bot
y : EReal
⊢ (⊥ + y).exp = ⊥.exp * y.exp

case h_real
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

case h_top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Proof state:
case h_top.h_real
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Tactic:
simp [Real.exp_pos]

Result:
no goals

Proof state:
case h_real.h_bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).exp = (↑a✝).exp * ⊥.exp

Tactic:
simp

Result:
no goals

Proof state:
case h_real.h_top
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Tactic:
simp [Real.exp_pos]

Result:
no goals

Proof state:
case h_bot
y : EReal
⊢ (⊥ + y).exp = ⊥.exp * y.exp

Tactic:
simp

Result:
no goals

Proof state:
case h_top.h_real
a✝ : ℝ
⊢ ⊤ = ⊤ * ENNReal.ofReal (Real.exp a✝)

Tactic:
rw [ENNReal.top_mul]

Result:
case h_top.h_real
a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp a✝) ≠ 0

Proof state:
case h_real
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

Tactic:
induction y

Result:
case h_real.h_bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).exp = (↑a✝).exp * ⊥.exp

case h_real.h_real
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

case h_real.h_top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Proof state:
case h_top.h_top

⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
simp

Result:
no goals

Proof state:
case h_top.h_bot

⊢ (⊤ + ⊥).exp = ⊤.exp * ⊥.exp

Tactic:
simp

Result:
no goals

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ ENNReal.ofReal (Real.exp (a✝¹ + a✝)) = ENNReal.ofReal (Real.exp a✝¹) * ENNReal.ofReal (Real.exp a✝)

Tactic:
rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_zero (nz) : normalize 0 d nz = 0

Proof state:
d : Nat
nz : d ≠ 0
⊢ normalize 0 d nz = 0

Tactic:
simp [normalize, Int.zero_tdiv, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]

Result:
d : Nat
nz : d ≠ 0
⊢ ↑0 = 0

Proof state:
d : Nat
nz : d ≠ 0
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m.lcm n ∣ k

Tactic:
apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))

Result:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m.gcd n * m.lcm n ∣ m.gcd n * k

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m * n ∣ (m * k).gcd (k * n)

Tactic:
exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)

Result:
no goals

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ m.lcm n ∣ 0

Tactic:
exact Nat.dvd_zero _

Result:
no goals

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m.gcd n * m.lcm n ∣ m.gcd n * k

Tactic:
rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]

Result:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m * n ∣ (m * k).gcd (k * n)

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
⊢ m.lcm n ∣ k

Tactic:
match eq_zero_or_pos k with
| .inl h => rw [h]; exact Nat.dvd_zero _
| .inr kpos =>
  apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
  rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
  exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)

Result:
no goals

Proof state:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ m.lcm n ∣ k

Tactic:
rw [h]

Result:
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ m.lcm n ∣ 0
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=
  letI := Classical.decEq R
  if h0 : (0 : R) = 1 then
    haveI := subsingleton_of_zero_eq_one h0
    Subsingleton.elim _ _
  else by
    have : p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ (p * q).Monic

Tactic:
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
  simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).Monic

Tactic:
rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] :
    #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β)

Proof state:
case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
apply mk_finsupp_lift_of_infinite

Result:
no goals

Proof state:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
rw [mk_finsupp_lift_of_fintype]

Result:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = lift.{v, u} #α ⊔ lift.{u, v} #β

Proof state:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)

Result:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{?u.16774, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = lift.{v, u} #α ⊔ lift.{u, v} #β

Proof state:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{?u.16774, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
rw [max_eq_right (le_trans _ this), power_nat_eq this]

Result:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀

Proof state:
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
cases fintypeOrInfinite α

Result:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Proof state:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀

Tactic:
exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem cg_iff_countable [Countable (Σl, L.Functions l)] {s : L.Substructure M} :
    s.CG ↔ Countable s

Proof state:
case intro.intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : Set M
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
exact h.substructure_closure L

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG ↔ Countable ↥s

Tactic:
refine ⟨?_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG → Countable ↥s

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG → Countable ↥s

Tactic:
rintro ⟨s, h, rfl⟩

Result:
case intro.intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : Set M
h : s.Countable
⊢ Countable ↥((closure L).toFun s)
-- Mathlib/Topology/List.lean
theorem tendsto_cons {n : ℕ} {a : α} {l : List.Vector α n} :
    Tendsto (fun p : α × List.Vector α n => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List.Vector α n
⊢ Tendsto (fun p => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))

Tactic:
rw [tendsto_subtype_rng, Vector.cons_val]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List.Vector α n
⊢ Tendsto (fun x => ↑(x.1 ::ᵥ x.2)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List.Vector α n
⊢ Tendsto (fun x => ↑(x.1 ::ᵥ x.2)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))

Tactic:
exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b)

Proof state:
⊢ ∀ (a b : Bool), (!(a && !b)) = (!a || b)

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
    ((a / b : ℚ).den : ℤ) = b

Proof state:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ ↑(↑a / ↑b).den = b

Tactic:
rw [← Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div,
  ← mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.single {I : Type*} [Fintype I] [DecidableEq I]
    (R : I → Type*) [∀ i, Semiring (R i)] :
    CompleteOrthogonalIdempotents (Pi.single (f := R) · 1)

Proof state:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
⊢ Pairwise fun x1 x2 => Pi.single x1 1 * Pi.single x2 1 = 0

Tactic:
intros i j hij

Result:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
⊢ Pi.single i 1 * Pi.single j 1 = 0

Proof state:
case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
⊢ (Pi.single i 1 * Pi.single j 1) i = 0 i

Tactic:
simp [hij]

Result:
no goals

Proof state:
case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Tactic:
subst hi

Result:
case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
⊢ (Pi.single i 1 * Pi.single j 1) i = 0 i

Proof state:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
⊢ CompleteOrthogonalIdempotents fun x => Pi.single x 1

Tactic:
refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩

Result:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
⊢ Pairwise fun x1 x2 => Pi.single x1 1 * Pi.single x2 1 = 0

Proof state:
case neg
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : ¬i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Tactic:
simp [hi]

Result:
no goals

Proof state:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
⊢ Pi.single i 1 * Pi.single j 1 = 0

Tactic:
ext k

Result:
case h
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Proof state:
case h
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Tactic:
by_cases hi : i = k

Result:
case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

case neg
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : ¬i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Proof state:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
⊢ ∀ (i : I), IsIdempotentElem (Pi.single i 1)

Tactic:
simp [IsIdempotentElem, ← Pi.single_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
protected lemma Nil.tail {p : G.Walk v w} (hp : p.Nil) : p.tail.Nil

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.tail.Nil

Tactic:
cases p <;> aesop

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
lemma e_ne_zero (t : IsSl2Triple h e f) : e ≠ 0

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : e = 0
⊢ h = 0

Tactic:
simpa [this] using t.lie_e_f.symm

Result:
no goals

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ e ≠ 0

Tactic:
have := t.h_ne_zero

Result:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ e ≠ 0

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ e ≠ 0

Tactic:
contrapose! this

Result:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : e = 0
⊢ h = 0
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma odd_matches_node_outside [Finite V] {u : Set V}
    {c : ConnectedComponent (Subgraph.deleteVerts ⊤ u).coe}
    (hM : M.IsPerfectMatching) (codd : Odd c.supp.ncard) :
    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.supp

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
⊢ (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) w ∧
    ∀ (y : V), (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) y → y = w

Tactic:
have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) w ∧
    ∀ (y : V), (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) y → y = w
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem mem_closure_isSwap' {f : Perm α} :
    f ∈ closure {σ : Perm α | σ.IsSwap} ↔ (fixedBy α f)ᶜ.Finite

Proof state:
case neg
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : ¬x = f x
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Tactic:
exact subset_closure ⟨x, f x, h, rfl⟩

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Tactic:
rw [← h, swap_self]

Result:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.refl α ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Proof state:
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
⊢ f ∈ closure {σ | σ.IsSwap} ↔ (fixedBy α f)ᶜ.Finite

Tactic:
refine (mem_closure_isSwap fun _ ↦ id).trans
  (and_iff_left fun x ↦ ⟨⟨swap x (f x), ?_⟩, swap_apply_left x (f x)⟩)

Result:
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Proof state:
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Tactic:
by_cases h : x = f x

Result:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

case neg
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : ¬x = f x
⊢ swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Proof state:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.refl α ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y

Tactic:
apply Subgroup.one_mem

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem empty_pi (s : ∀ i, Set (α i)) : pi ∅ s = univ

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ ∅.pi s ↔ x✝ ∈ univ

Tactic:
simp [pi]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ ∅.pi s = univ

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ ∅.pi s ↔ x✝ ∈ univ
-- Mathlib/Data/Rat/Floor.lean
theorem isNat_intCeil {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℕ) :
    IsNat r m → IsNat ⌈r⌉ m

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ ⌈↑m⌉ = ↑m

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌈r⌉ m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m

Proof state:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m

Tactic:
exact ⟨by simp⟩

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem HasBasis.liminf_eq_sSup_iUnion_iInter {ι ι' : Type*} {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :
    liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i))

Proof state:
case e_a.h
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
x : α
⊢ x ∈ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} ↔ x ∈ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
simp only [mem_setOf_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists,
  exists_prop]

Result:
no goals

Proof state:
case e_a
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
ext x

Result:
case e_a.h
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
x : α
⊢ x ∈ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} ↔ x ∈ ⋃ j, ⋂ i, Iic (f ↑i)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ liminf f v = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Tactic:
simp_rw [liminf_eq, hv.eventually_iff]

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ sSup {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ sSup {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = ⋃ j, ⋂ i, Iic (f ↑i)