harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic)
    (p_gen : Ideal.span {p} = annIdeal 𝕜 a) : annIdealGenerator 𝕜 a = p

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen

Result:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a

Tactic:
apply eq_of_monic_of_associated p_monic _ p_gen

Result:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ (annIdealGenerator 𝕜 a).Monic

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
⊢ annIdealGenerator 𝕜 a = p

Tactic:
by_cases h : p = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p

case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rw [eq_comm]

Result:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ (annIdealGenerator 𝕜 a).Monic

Tactic:
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_one' {h : Decidable (1 : PartENat).Dom} : toWithTop 1 = 1

Proof state:
h : Decidable (Dom 1)
⊢ toWithTop 1 = 1

Tactic:
convert toWithTop_one

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_ceil_right_pure_add_one (n : ℤ) :
    Tendsto (ceil : α → ℤ) (𝓝[>] n) (pure (n + 1))

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[>] ↑n) (pure (n + 1))

Tactic:
simpa only [floor_intCast] using tendsto_ceil_right_pure_floor_add_one (n : α)

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_left_inj (h : IsUnit c) : a / c = b / c ↔ a = b

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b

Tactic:
exact Units.mul_left_inj h.inv.unit'

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b

Tactic:
simp only [div_eq_mul_inv]

Result:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem Finsupp.mul_sum (b : S) (s : α →₀ R) {f : α → R → S} :
    b * s.sum f = s.sum fun a c => b * f a c

Proof state:
α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * s.sum f = s.sum fun a c => b * f a c

Tactic:
simp only [Finsupp.sum, Finset.mul_sum]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/CompTypeclasses.lean
lemma comp_inv {φ : M →* N} {ψ : N →* M} (h : Function.RightInverse φ ψ)
    {χ : M →* M} [IsId χ] :
    CompTriple φ ψ χ where
  comp_eq

Proof state:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse ⇑φ ⇑ψ
χ : M →* M
inst✝ : IsId χ
⊢ _root_.id = ⇑(id M)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse ⇑φ ⇑ψ
χ : M →* M
inst✝ : IsId χ
⊢ ψ.comp φ = χ

Tactic:
simp only [IsId.eq_id, ← DFunLike.coe_fn_eq, coe_comp, h.id]

Result:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse ⇑φ ⇑ψ
χ : M →* M
inst✝ : IsId χ
⊢ _root_.id = ⇑(id M)
-- Mathlib/Data/List/Sigma.lean
theorem head?_lookupAll (a : α) : ∀ l : List (Sigma β), head? (lookupAll a l) = dlookup a l
  | [] => by simp
  | ⟨a', b⟩ :: l => by
    by_cases h : a = a'
    · subst h; simp
    · rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l] <;> assumption

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

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'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (lookupAll a []).head? = dlookup a []

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
subst h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l] <;> assumption

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem eq_padicNorm (q : ℚ) : ‖(q : ℚ_[p])‖ = padicNorm p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ‖↑q‖ = ↑(padicNorm p q)

Tactic:
dsimp [norm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ↑(padicNormE ↑q) = ↑(padicNorm p q)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ↑(padicNormE ↑q) = ↑(padicNorm p q)

Tactic:
rw [← padicNormE.eq_padic_norm']

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
@[to_additive] lemma prod_sigma_eq_prod {α : Type*} [CommMonoid α] (v : Fin n → α) :
    ∏ (m : Fin c.length), ∏ (r : Fin (c.partSize m)), v (c.emb m r) = ∏ i, v i

Proof state:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst✝ : CommMonoid α
v : Fin n → α
⊢ ∏ x ∈ Finset.univ.sigma fun m => Finset.univ, v (c.emb x.fst x.snd) = ∏ i : Fin n, v i

Tactic:
exact Fintype.prod_equiv c.equivSigma _ _ (fun p ↦ rfl)

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst✝ : CommMonoid α
v : Fin n → α
⊢ ∏ m : Fin c.length, ∏ r : Fin (c.partSize m), v (c.emb m r) = ∏ i : Fin n, v i

Tactic:
rw [Finset.prod_sigma']

Result:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst✝ : CommMonoid α
v : Fin n → α
⊢ ∏ x ∈ Finset.univ.sigma fun m => Finset.univ, v (c.emb x.fst x.snd) = ∏ i : Fin n, v i
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_neg_right : (f =O[l] fun x => -g' x) ↔ f =O[l] g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x => -g' x) ↔ ∃ c, IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_neg_right

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x => -g' x) ↔ f =O[l] g'

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x => -g' x) ↔ ∃ c, IsBigOWith c l f g'
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_lt_ofNat : (p : K) < ofNat(n) ↔ p < OfNat.ofNat n

Proof state:
K : Type u_5
inst✝¹ : LinearOrderedSemifield K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n

Tactic:
simp [← cast_lt (K := K)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem mem_closure_iff_iSup :
    a ∈ closure s ↔
      ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal), (∀ i, f i ∈ s) ∧ ⨆ i, f i = a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) ↔
    ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
simp_rw [exists_prop]

Result:
no goals

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
apply ((mem_closure_tfae a s).out 0 5).trans

Result:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) ↔
    ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m

Proof state:
n m : Nat
⊢ n.succ * m = n * m + m

Tactic:
induction m with
| zero => rfl
| succ m ih => rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm]

Result:
no goals

Proof state:
case zero
n : Nat
⊢ n.succ * 0 = n * 0 + 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n m : Nat
ih : n.succ * m = n * m + m
⊢ n.succ * (m + 1) = n * (m + 1) + (m + 1)

Tactic:
rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_embDomain : (s.embDomain f).hsum = s.hsum

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (s.embDomain f).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ⇑f then (s (Classical.choose ⋯)).coeff g else 0) = ∑ᶠ (i : α), (s i).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ⇑f then (s (Classical.choose ⋯)).coeff g else 0) = ∑ᶠ (i : α), (s i).coeff g

Tactic:
exact finsum_emb_domain f fun a => (s a).coeff g

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
⊢ (s.embDomain f).hsum = s.hsum

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (s.embDomain f).hsum.coeff g = s.hsum.coeff g

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
⊢ (s.embDomain f).hsum = s.hsum

Tactic:
classical
ext g
simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
exact finsum_emb_domain f fun a => (s a).coeff g

Result:
no goals
-- Mathlib/Algebra/Homology/DifferentialObject.lean
theorem objEqToHom_d {x y : β} (h : x = y) :
    X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom (by cases h; rfl)

Proof state:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom ⋯

Tactic:
cases h

Result:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯

Proof state:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ 𝟙 (X.obj x) ≫ X.d x = X.d x ≫ 𝟙 (X.obj (x + 1 • b))

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1279, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) y

Tactic:
cases h

Result:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1279, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x

Proof state:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1279, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x

Tactic:
rfl

Result:
no goals

Proof state:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯

Tactic:
dsimp

Result:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ 𝟙 (X.obj x) ≫ X.d x = X.d x ≫ 𝟙 (X.obj (x + 1 • b))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_mapIdx_iff {l : Array α} :
    mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.size) → f i l[i] = g i l[i]

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ mapIdx f { toList := l } = mapIdx g { toList := l } ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = g i { toList := l }[i]

Tactic:
simp [List.mapIdx_eq_mapIdx_iff]

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : Array α
⊢ mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] = g i l[i]

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ mapIdx f { toList := l } = mapIdx g { toList := l } ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = g i { toList := l }[i]
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.measure_zero_or_one_of_measurableSet_limsup (h_le : ∀ n, s n ≤ m0)
    (h_indep : iIndep s κ μα)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a))
    (hns_univ : ∀ n, ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
  ((indep_limsup_self h_le h_indep hf hns hnsp hns_univ).indepSet_of_measurableSet ht_tail
    ht_tail)

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
@[simp]
lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow

Proof state:
n : ℤ
⊢ (n * n).negOnePow = n.negOnePow

Tactic:
simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem toPretrivialization_injective :
    Function.Injective fun e : Trivialization F proj => e.toPretrivialization := fun e e' h => by
  ext1
  exacts [PartialHomeomorph.toPartialEquiv_injective (congr_arg Pretrivialization.toPartialEquiv h),
    congr_arg Pretrivialization.baseSet h]

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'
⊢ e = e'

Tactic:
ext1

Result:
case h₁
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'
⊢ e.toPartialHomeomorph = e'.toPartialHomeomorph

case h₂
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'
⊢ e.baseSet = e'.baseSet

Proof state:
case h₁
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'
⊢ e.toPartialHomeomorph = e'.toPartialHomeomorph

case h₂
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'
⊢ e.baseSet = e'.baseSet

Tactic:
exacts [PartialHomeomorph.toPartialEquiv_injective (congr_arg Pretrivialization.toPartialEquiv h),
  congr_arg Pretrivialization.baseSet h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_sublist_right {s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n :=
  ⟨fun h => by simpa only [length_range'] using h.length_le,
   fun h => by rw [← add_sub_of_le h, ← range'_append]; apply sublist_append_left⟩

Proof state:
step s m n : Nat
h : range' s m step <+ range' s n step
⊢ m ≤ n

Tactic:
simpa only [length_range'] using h.length_le

Result:
no goals

Proof state:
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s n step

Tactic:
rw [← add_sub_of_le h, ← range'_append]

Result:
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s m step ++ range' (s + step * m) (n - m) step

Proof state:
step s m n : Nat
h : m ≤ n
⊢ range' s m step <+ range' s m step ++ range' (s + step * m) (n - m) step

Tactic:
apply sublist_append_left

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
@[simp]
lemma sq_nonpos_iff [IsRightCancelAdd α] [ZeroLEOneClass α] [ExistsAddOfLE α]
    [PosMulMono α] [AddLeftStrictMono α] [NoZeroDivisors α] (r : α) :
    r ^ 2 ≤ 0 ↔ r = 0

Proof state:
α : Type u
inst✝⁷ : Semiring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsRightCancelAdd α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : NoZeroDivisors α
r : α
⊢ r ^ 2 = 0 ↔ r = 0

Tactic:
exact sq_eq_zero_iff

Result:
no goals

Proof state:
α : Type u
inst✝⁷ : Semiring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsRightCancelAdd α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : NoZeroDivisors α
r : α
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 = 0

Tactic:
rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]

Result:
no goals

Proof state:
α : Type u
inst✝⁷ : Semiring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsRightCancelAdd α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : NoZeroDivisors α
r : α
⊢ r ^ 2 ≤ 0 ↔ r = 0

Tactic:
trans r ^ 2 = 0

Result:
α : Type u
inst✝⁷ : Semiring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsRightCancelAdd α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : NoZeroDivisors α
r : α
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 = 0

α : Type u
inst✝⁷ : Semiring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsRightCancelAdd α
inst✝⁴ : ZeroLEOneClass α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : NoZeroDivisors α
r : α
⊢ r ^ 2 = 0 ↔ r = 0