harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem evalFacProps {l : Products I} (J K : I → Prop)
    (h : ∀ a, a ∈ l.val → J a) [∀ j, Decidable (J j)] [∀ j, Decidable (K j)]
    (hJK : ∀ i, J i → K i) :
    l.eval (π C J) ∘ ProjRestricts C hJK = l.eval (π C K)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
⊢ ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)

Tactic:
ext

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
x✝ : ↑(π (π C K) J)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) x✝ = (eval (π (π C K) J) l) x✝

Proof state:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)

Tactic:
rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h]

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
⊢ ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)

Tactic:
have : l.eval (π C J) ∘ Homeomorph.setCongr (proj_eq_of_subset C J K hJK) =
    l.eval (π (π C K) J) := by
  ext; simp [Homeomorph.setCongr, Products.eval_eq]

Result:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)
⊢ ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
x✝ : ↑(π (π C K) J)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) x✝ = (eval (π (π C K) J) l) x✝

Tactic:
simp [Homeomorph.setCongr, Products.eval_eq]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_add_omega0 (n : ℕ) : n + ω = ω

Proof state:
case intro.intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ ↑n + ↑m < ω

Tactic:
exact_mod_cast nat_lt_omega0 (n + m)

Result:
no goals

Proof state:
case intro.intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ a < ω

Tactic:
apply hb.trans_lt

Result:
case intro.intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ ↑n + ↑m < ω

Proof state:
n : ℕ
⊢ ↑n + ω = ω

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha ↦ ?_) (le_add_left _ _)

Result:
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
⊢ a < ω

Proof state:
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
⊢ a < ω

Tactic:
obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha

Result:
case intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
b : Ordinal.{u_1}
hb' : b < ω
hb : a ≤ ↑n + b
⊢ a < ω

Proof state:
case intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
b : Ordinal.{u_1}
hb' : b < ω
hb : a ≤ ↑n + b
⊢ a < ω

Tactic:
obtain ⟨m, rfl⟩ := lt_omega0.1 hb'

Result:
case intro.intro.intro
n : ℕ
a : Ordinal.{u_1}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ a < ω
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem coe_primesOverFinset : primesOverFinset p B = primesOver p B

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
⊢ ↑(primesOverFinset p B) = p.primesOver B

Tactic:
ext P

Result:
case h
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
P : Ideal B
⊢ P ∈ ↑(primesOverFinset p B) ↔ P ∈ p.primesOver B

Proof state:
case h
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
P : Ideal B
⊢ P ∈ normalizedFactors (map (algebraMap A B) p) ↔ P ∈ p.primesOver B

Tactic:
exact (P.mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hpb)).trans <| Iff.intro
  (fun ⟨hPp, h⟩ => ⟨hPp, ⟨hpm.eq_of_le (comap_ne_top _ hPp.ne_top) (le_comap_of_map_le h)⟩⟩)
  (fun ⟨hPp, h⟩ => ⟨hPp, map_le_of_le_comap h.1.le⟩)

Result:
no goals

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
⊢ ↑(primesOverFinset p B) = p.primesOver B

Tactic:
classical
ext P
rw [primesOverFinset, factors_eq_normalizedFactors, Finset.mem_coe, Multiset.mem_toFinset]
exact (P.mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hpb)).trans <| Iff.intro
  (fun ⟨hPp, h⟩ => ⟨hPp, ⟨hpm.eq_of_le (comap_ne_top _ hPp.ne_top) (le_comap_of_map_le h)⟩⟩)
  (fun ⟨hPp, h⟩ => ⟨hPp, map_le_of_le_comap h.1.le⟩)

Result:
no goals

Proof state:
case h
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
P : Ideal B
⊢ P ∈ ↑(primesOverFinset p B) ↔ P ∈ p.primesOver B

Tactic:
rw [primesOverFinset, factors_eq_normalizedFactors, Finset.mem_coe, Multiset.mem_toFinset]

Result:
case h
A : Type u_4
inst✝⁴ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝³ : CommRing B
inst✝² : IsDedekindDomain B
inst✝¹ : Algebra A B
inst✝ : NoZeroSMulDivisors A B
P : Ideal B
⊢ P ∈ normalizedFactors (map (algebraMap A B) p) ↔ P ∈ p.primesOver B
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_orderOf_eq_one (x : G) : x ^ orderOf x = 1

Proof state:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = x ^ minimalPeriod (fun x_1 => x * x_1) 1 * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = (fun x_1 => x * x_1)^[minimalPeriod (fun x_1 => x * x_1) 1] 1

Tactic:
rw [orderOf, mul_left_iterate]

Result:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = (fun x_1 => x ^ minimalPeriod (fun x_2 => x * x_2) 1 * x_1) 1

Proof state:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = (fun x_1 => x ^ minimalPeriod (fun x_2 => x * x_2) 1 * x_1) 1

Tactic:
beta_reduce

Result:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = x ^ minimalPeriod (fun x_1 => x * x_1) 1 * 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findRevM?_eq_findM?_reverse
    [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) :
    as.findRevM? f = as.reverse.findM? f

Proof state:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
toList✝ : List α
⊢ findRevM? f { toList := toList✝ } = findM? f { toList := toList✝ }.reverse

Tactic:
rw [List.findRevM?_toArray]

Result:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
toList✝ : List α
⊢ List.findM? f toList✝.reverse = findM? f { toList := toList✝ }.reverse

Proof state:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
as : Array α
⊢ findRevM? f as = findM? f as.reverse

Tactic:
cases as

Result:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
toList✝ : List α
⊢ findRevM? f { toList := toList✝ } = findM? f { toList := toList✝ }.reverse

Proof state:
case mk
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
toList✝ : List α
⊢ List.findM? f toList✝.reverse = findM? f { toList := toList✝ }.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma shiftₗ_pow_apply (f : M → G) (k : ℕ) (y : M) : (shiftₗ M G h ^ k) f y = f (y + k • h)

Proof state:
case succ
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
k : ℕ
IH : ∀ (f : M → G), (shiftₗ M G h ^ k) f y = f (y + k • h)
f : M → G
⊢ (shiftₗ M G h ^ (k + 1)) f y = f (y + (k + 1) • h)

Tactic:
simp only [pow_add, pow_one, LinearMap.mul_apply, IH (shiftₗ M G h f), shiftₗ_apply, add_assoc,
  add_nsmul, one_smul]

Result:
no goals

Proof state:
case zero
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
f : M → G
⊢ (shiftₗ M G h ^ 0) f y = f (y + 0 • h)

Tactic:
simp only [pow_zero, LinearMap.one_apply, cast_zero, add_zero, zero_smul]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
k : ℕ
y : M
⊢ (shiftₗ M G h ^ k) f y = f (y + k • h)

Tactic:
induction' k with k IH generalizing f

Result:
case zero
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
f : M → G
⊢ (shiftₗ M G h ^ 0) f y = f (y + 0 • h)

case succ
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
k : ℕ
IH : ∀ (f : M → G), (shiftₗ M G h ^ k) f y = f (y + k • h)
f : M → G
⊢ (shiftₗ M G h ^ (k + 1)) f y = f (y + (k + 1) • h)
-- Mathlib/LinearAlgebra/Dual.lean
lemma dualMap_dualMap_eq_iff_of_injective
    {M' : Type*} [AddCommGroup M'] [Module R M'] {f g : M →ₗ[R] M'}
    (h : Injective (Dual.eval R M')) :
    f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g

Tactic:
exact hfg

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
simp only [← Dual.eval_comp_comp_evalEquiv_eq]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
⊢ Dual.eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = Dual.eval R M' ∘ₗ g ∘ₗ ↑(evalEquiv R M).symm ↔ f = g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : Dual.eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = Dual.eval R M' ∘ₗ g ∘ₗ ↑(evalEquiv R M).symm
⊢ f = g

Tactic:
rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
⊢ Dual.eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = Dual.eval R M' ∘ₗ g ∘ₗ ↑(evalEquiv R M).symm ↔ f = g

Tactic:
refine ⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
  (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_4
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : Dual.eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = Dual.eval R M' ∘ₗ g ∘ₗ ↑(evalEquiv R M).symm
⊢ f = g
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.conj : SameCycle f x y → SameCycle (g * f * g⁻¹) (g x) (g y)

Proof state:
α : Type u_2
f g : Perm α
x y : α
⊢ f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)

Tactic:
simp [sameCycle_conj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_eq_getElem? : ∀ (l : List α), getLast? l = l[l.length - 1]?
  | [] => rfl
  | a::l => by
    rw [getLast?_eq_getLast (a::l) nofun, getLast_eq_getElem, getElem?_eq_getElem]

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).getLast? = (a :: l)[(a :: l).length - 1]?

Tactic:
rw [getLast?_eq_getLast (a::l) nofun, getLast_eq_getElem, getElem?_eq_getElem]

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem hasMellin_add {f g : ℝ → E} {s : ℂ} (hf : MellinConvergent f s)
    (hg : MellinConvergent g s) : HasMellin (fun t => f t + g t) s (mellin f s + mellin g s) :=
  ⟨by simpa only [MellinConvergent, smul_add] using hf.add hg, by
    simpa only [mellin, smul_add] using integral_add hf hg⟩

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ MellinConvergent (fun t => f t + g t) s

Tactic:
simpa only [MellinConvergent, smul_add] using hf.add hg

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ mellin (fun t => f t + g t) s = mellin f s + mellin g s

Tactic:
simpa only [mellin, smul_add] using integral_add hf hg

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma pi_lex_lt_cons_cons {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ}
    (s : ∀ {i : Fin n.succ}, α i → α i → Prop) :
    Pi.Lex (· < ·) (@s) (Fin.cons x₀ x) (Fin.cons y₀ y) ↔
      s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (· < ·) (@fun i : Fin n ↦ @s i.succ) x y

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ Pi.Lex (fun x1 x2 => x1 < x2) s (cons x₀ x) (cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i => s) x y

Tactic:
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_iff_succ]

Result:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨
      ∃ i,
        ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ j < i, x j = y j) ∧ s (x i) (y i)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨
      ∃ i,
        ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ j < i, x j = y j) ∧ s (x i) (y i)

Tactic:
simp [and_assoc, exists_and_left]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
@[simp]
lemma valMinAbs_zero : ∀ n, (0 : ZMod n).valMinAbs = 0
  | 0 => by simp only [valMinAbs_def_zero]
  | n + 1 => by simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]

Proof state:
n : ℕ
⊢ valMinAbs 0 = 0

Tactic:
simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]

Result:
no goals

Proof state:
⊢ valMinAbs 0 = 0

Tactic:
simp only [valMinAbs_def_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_right_min {a b : Nat} : min (a + b) a = a

Proof state:
a b : Nat
⊢ min (a + b) a = a

Tactic:
rw [Nat.min_comm, min_add_right]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem one_leftCoset : (1 : α) • s = s :=
  Set.ext <| by simp [← image_smul]

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ 1 • s ↔ x ∈ s

Tactic:
simp [← image_smul]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem mem_compression_of_insert_mem_compression (h : insert a s ∈ 𝓓 a 𝒜) : s ∈ 𝓓 a 𝒜

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜

Tactic:
rwa [insert_eq_of_mem ha] at h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜

Tactic:
exact erase_mem_compression_of_mem_compression h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜

case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜

Tactic:
rw [← erase_insert ha]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜
-- Mathlib/Algebra/Order/Star/Basic.lean
/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.

This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
`StarOrderedRing.of_nonneg_iff` for a more convenient version.
-/
lemma of_le_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
    (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
  le_iff x y

Proof state:
case refine_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ (∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p) → x ≤ y

Tactic:
rintro ⟨p, hp, hpxy⟩

Result:
case refine_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
hpxy : y = x + p
⊢ x ≤ y
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem sameRay_iff_inv_norm_smul_eq : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Proof state:
case inr.inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0

Tactic:
simp [SameRay.zero_right]

Result:
no goals

Proof state:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y

Tactic:
simp [SameRay.zero_left]

Result:
no goals

Proof state:
case inr.inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
simp only [sameRay_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]

Result:
no goals

Proof state:
case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Result:
case inr.inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0

case inr.inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y

case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_eq_empty_iff (v : Vector α n) : v.toList = [] ↔ n = 0

Proof state:
α : Type u_1
n : Nat
h : #[].size = n
⊢ n = 0

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ { toArray := v, size_toArray := h }.toList = [] ↔ n = 0

Tactic:
simp only [Array.toList_eq_nil_iff]

Result:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ v = #[] ↔ n = 0

Proof state:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ v = #[] ↔ n = 0

Tactic:
exact ⟨by rintro rfl; simp_all, by rintro rfl; simpa using h⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ v = #[] → n = 0

Tactic:
rintro rfl

Result:
α : Type u_1
n : Nat
h : #[].size = n
⊢ n = 0

Proof state:
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ n = 0 → v = #[]

Tactic:
rintro rfl

Result:
α : Type u_1
v : Array α
h : v.size = 0
⊢ v = #[]

Proof state:
α : Type u_1
n : Nat
v : Vector α n
⊢ v.toList = [] ↔ n = 0

Tactic:
rcases v with ⟨v, h⟩

Result:
case mk
α : Type u_1
n : Nat
v : Array α
h : v.size = n
⊢ { toArray := v, size_toArray := h }.toList = [] ↔ n = 0

Proof state:
α : Type u_1
v : Array α
h : v.size = 0
⊢ v = #[]

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem append_nil {α} (xs : LazyList α) : xs.append (Thunk.pure LazyList.nil) = xs

Proof state:
case nil
α : Type u_1
⊢ nil.append (Thunk.pure nil) = nil

Tactic:
simp only [Thunk.pure, append, Thunk.get]

Result:
no goals

Proof state:
case mk
α : Type u_1
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), (fn✝ a).append (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => { fn := fn✝ }.get.append (Thunk.pure nil) } = { fn := fn✝ }

Tactic:
ext

Result:
case mk.a
α : Type u_1
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), (fn✝ a).append (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => { fn := fn✝ }.get.append (Thunk.pure nil) }.get = { fn := fn✝ }.get

Proof state:
case mk.a
α : Type u_1
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), (fn✝ a).append (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => { fn := fn✝ }.get.append (Thunk.pure nil) }.get = { fn := fn✝ }.get

Tactic:
apply ih

Result:
no goals

Proof state:
α : Type u_1
xs : LazyList α
⊢ xs.append (Thunk.pure nil) = xs

Tactic:
induction xs using LazyList.rec with
| nil => simp only [Thunk.pure, append, Thunk.get]
| cons _ _ => simpa only [append, cons.injEq, true_and]
| mk _ ih => ext; apply ih

Result:
no goals

Proof state:
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.44234 tl✝
⊢ (cons hd✝ tl✝).append (Thunk.pure nil) = cons hd✝ tl✝

Tactic:
simpa only [append, cons.injEq, true_and]

Result:
no goals