harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_iff_of_Y_eq_negY {P : Fin 3 → F} (hPz : P z ≠ 0) (hy : P y = W.negY P) :
    W.Nonsingular P ↔ W.Equation P ∧ eval P W.polynomialX ≠ 0

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = (P y - W.negY P) * P z
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = (P y - W.negY P) * P z

Tactic:
rw [negY, eval_polynomialY]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
have hy' : eval P W.polynomialY = (P y - W.negY P) * P z := by rw [negY, eval_polynomialY]; ring1

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = (P y - W.negY P) * P z
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem pnatCast_one [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ((1 : ℕ+) : Rˣ) = 1

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑⋯.unit = 1

Tactic:
rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = ↑1

Tactic:
rw [Units.val_one]

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑1 = 1

Tactic:
apply Units.ext

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = ↑1

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1

Tactic:
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑⋯.unit = 1

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1

Tactic:
rw [PNat.one_coe, Nat.cast_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem ne_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y ≠ 0
⊢ x ≠ y

Tactic:
rintro rfl

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x x ≠ 0
⊢ False

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x x ≠ 0
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Data/Set/Function.lean
protected lemma MapsTo.extendDomain (h : MapsTo g s t) :
    MapsTo (g.extendDomain f) ((↑) ∘ f '' s) ((↑) ∘ f '' t)

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
⊢ MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (Subtype.val ∘ ⇑f) (g a) = (g.extendDomain f) ((Subtype.val ∘ ⇑f) a)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t

Tactic:
exact ⟨_, h ha, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
/-- Two equivalent ways to express the evaluation of a bivariate polynomial over `R`
at a point in the affine plane over an `R`-algebra `S`. -/
lemma eval₂RingHom_eval₂RingHom (f : R →+* S) (x y : S) :
    eval₂RingHom (eval₂RingHom f x) y =
      (evalEvalRingHom x y).comp (mapRingHom <| mapRingHom f)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toFinset_toMultiset [DecidableEq α] (f : α →₀ ℕ) : f.toMultiset.toFinset = f.support

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (toMultiset (single a n + f)).toFinset = (single a n + f).support

Tactic:
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
  support_single_ne_zero _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint (single a n).support f.support

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset f).toFinset = f.support

Tactic:
refine f.induction ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset 0).toFinset = support 0

case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset 0).toFinset = support 0

Tactic:
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint {a} f.support

Tactic:
rwa [Finset.disjoint_singleton_left]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support

Tactic:
intro a n f ha hn ih

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (toMultiset (single a n + f)).toFinset = (single a n + f).support

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint (single a n).support f.support

Tactic:
refine Disjoint.mono_left support_single_subset ?_

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint {a} f.support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_filterMap' (f : α → Option β) (g : β → γ → γ) (l : Array α) (init : γ)
    (w : start = (l.filterMap f).size) :
    (l.filterMap f).foldr g init start 0 = l.foldr (fun x y => match f x with | some b => g b y | none => y) init

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
l : Array α
init : γ
⊢ foldr g init (filterMap f l) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
toList✝ : List α
⊢ foldr g init (filterMap f { toList := toList✝ }) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
toList✝ : List α
⊢ List.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init toList✝ =
    List.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init toList✝

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
toList✝ : List α
⊢ foldr g init (filterMap f { toList := toList✝ }) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init { toList := toList✝ }

Tactic:
simp [List.foldr_filterMap]

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
toList✝ : List α
⊢ List.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init toList✝ =
    List.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init toList✝

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
start : Nat
f : α → Option β
g : β → γ → γ
l : Array α
init : γ
w : start = (filterMap f l).size
⊢ foldr g init (filterMap f l) start =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
l : Array α
init : γ
⊢ foldr g init (filterMap f l) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_eq_zero_iff : ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Proof state:
case empty
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ ∅, f x = 0 ↔ ∃ a ∈ ∅, f a = 0

Tactic:
exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩

Result:
no goals

Proof state:
case insert
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a✝ : ι
s✝ : Finset ι
ha : a✝ ∉ s✝
ih : ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ s✝, f a = 0
⊢ ∏ x ∈ insert a✝ s✝, f x = 0 ↔ ∃ a ∈ insert a✝ s✝, f a = 0

Tactic:
rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x✝ : ∃ a ∈ ∅, f a = 0
w✝ : ι
H : w✝ ∈ ∅
right✝ : f w✝ = 0
⊢ ∏ x ∈ ∅, f x = 0

Tactic:
simp at H

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
induction s using Finset.induction_on with
| empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
| insert ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
  | insert ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem WeakDual.CharacterSpace.exists_apply_eq_zero {a : A} (ha : ¬IsUnit a) :
    ∃ f : characterSpace ℂ A, f a = 0

Proof state:
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
ha : ¬IsUnit a
⊢ ∃ f, f a = 0

Tactic:
obtain ⟨M, hM, haM⟩ := (span {a}).exists_le_maximal (span_singleton_ne_top ha)

Result:
case intro.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
ha : ¬IsUnit a
M : Ideal A
hM : M.IsMaximal
haM : span {a} ≤ M
⊢ ∃ f, f a = 0

Proof state:
case intro.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
ha : ¬IsUnit a
M : Ideal A
hM : M.IsMaximal
haM : span {a} ≤ M
⊢ ∃ f, f a = 0

Tactic:
exact
  ⟨M.toCharacterSpace,
    M.toCharacterSpace_apply_eq_zero_of_mem
      (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩

Result:
no goals
-- Mathlib/Control/Monad/Cont.lean
theorem ReaderT.goto_mkLabel {α ρ β} (x : Label α m β) (i : α) :
    goto (ReaderT.mkLabel ρ x) i = monadLift (goto x i)

Proof state:
case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
cases x

Result:
case mk
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)
-- Mathlib/Algebra/CharP/Defs.lean
lemma intCast_eq_zero_iff (a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a

Proof state:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]

Result:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ -a

Proof state:
case inr.inr.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h✝ h : 0 < ↑b
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b

Tactic:
rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Result:
no goals

Proof state:
case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0

Tactic:
simp only [Int.cast_zero, eq_self_iff_true, Int.dvd_zero]

Result:
no goals

Proof state:
case inl.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b

Tactic:
rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
rcases lt_trichotomy a 0 with (h | rfl | h)

Result:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a

case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0

case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Proof state:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ -a

Tactic:
lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b

Result:
case inl.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b

Proof state:
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
lift a to ℕ using le_of_lt h with b

Result:
case inr.inr.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h✝ h : 0 < ↑b
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
-- Mathlib/Data/List/GetD.lean
theorem getD_reverse {l : List α} (i) (h : i < length l) :
    getD l.reverse i = getD l (l.length - 1 - i)

Proof state:
case h
α : Type u
l : List α
i : ℕ
h : i < l.length
a : α
⊢ l.reverse.getD i a = l.getD (l.length - 1 - i) a

Tactic:
rwa [List.getD_eq_getElem?_getD, List.getElem?_reverse, ← List.getD_eq_getElem?_getD]

Result:
no goals

Proof state:
α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ l.reverse.getD i = l.getD (l.length - 1 - i)

Tactic:
funext a

Result:
case h
α : Type u
l : List α
i : ℕ
h : i < l.length
a : α
⊢ l.reverse.getD i a = l.getD (l.length - 1 - i) a
-- Mathlib/MeasureTheory/Integral/Indicator.lean
/-- If `μ` is a finite measure and the indicators of measurable sets `Aᵢ` tend pointwise to
the indicator of a set `A`, then the measures `μ Aᵢ` tend to the measure `μ A`. -/
lemma tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure
    (μ : Measure α) [IsFiniteMeasure μ] (As_mble : ∀ i, MeasurableSet (As i))
    (h_lim : ∀ x, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) :
    Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i => μ (As i)) L (𝓝 (μ A))

Tactic:
rcases L.eq_or_neBot with rfl | _

Result:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst✝ : ⊥.IsCountablyGenerated
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i => μ (As i)) ⊥ (𝓝 (μ A))

case inr
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i => μ (As i)) L (𝓝 (μ A))

Proof state:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst✝ : ⊥.IsCountablyGenerated
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i => μ (As i)) ⊥ (𝓝 (μ A))

Tactic:
exact tendsto_bot

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ MeasurableSet A

Tactic:
exact measurableSet_of_tendsto_indicator L As_mble h_lim

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i => μ (As i)) L (𝓝 (μ A))

Tactic:
apply tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure L ?_ As_mble (ae_of_all μ h_lim)

Result:
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ MeasurableSet A
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_toFinset_prod (f : α → M) (s : Set α) [Fintype s] :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ s.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp_rw [coe_toFinset s]

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f

Tactic:
simp_rw [coe_toFinset s]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
@[to_additive (attr := simp) sub_mem_addCentralizer]
lemma div_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a / b ∈ centralizer S

Proof state:
M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
@[to_additive]
lemma prod_eq_one (h : ∀ x ∈ s, x = (1 : α)) : s.prod = 1

Proof state:
case h
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x = 1
⊢ prod ⟦a✝⟧ = 1

Tactic:
simp [List.prod_eq_one h]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
h : ∀ x ∈ s, x = 1
⊢ s.prod = 1

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x = 1
⊢ prod ⟦a✝⟧ = 1
-- Mathlib/Data/Set/Pointwise/Support.lean
theorem support_comp_inv_smul [Zero γ] (c : α) (f : β → γ) :
    (support fun x ↦ f (c⁻¹ • x)) = c • support f

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem, mem_support]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpFamily_le_apply [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b

Tactic:
push_neg

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b

Tactic:
rw [← not_iff_not]

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
exact apply_lt_nfpFamily_iff H

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Filter.Tendsto.div_const {x : G₀} (hf : Tendsto f l (𝓝 x)) (y : G₀) :
    Tendsto (fun a => f a / y) l (𝓝 (x / y))

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝² : DivInvMonoid G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousMul G₀
f : α → G₀
l : Filter α
x : G₀
hf : Tendsto f l (𝓝 x)
y : G₀
⊢ Tendsto (fun a => f a / y) l (𝓝 (x / y))

Tactic:
simpa only [div_eq_mul_inv] using hf.mul tendsto_const_nhds

Result:
no goals