harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/EReal.lean
lemma mul_ne_top (a b : EReal) :
    a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
set_option push_neg.use_distrib true in push_neg

Result:
a b : EReal
⊢ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rfl

Result:
no goals

Proof state:
a b : EReal
⊢ ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
push_neg

Result:
a b : EReal
⊢ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_top]

Result:
a b : EReal
⊢ ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_two_pi : sin (2 * π) = 0

Proof state:
⊢ sin (2 * π) = 0

Tactic:
simp [two_mul, sin_add]

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
lemma pathComponentIn_mem_nhds (hF : F ∈ 𝓝 x) : pathComponentIn x F ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : X
F : Set X
inst✝ : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
⊢ pathComponentIn x F ∈ 𝓝 x

Tactic:
let ⟨u, huF, hu, hxu⟩ := mem_nhds_iff.mp hF

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : X
F : Set X
inst✝ : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
u : Set X
huF : u ⊆ F
hu : IsOpen u
hxu : x ∈ u
⊢ pathComponentIn x F ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : X
F : Set X
inst✝ : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
u : Set X
huF : u ⊆ F
hu : IsOpen u
hxu : x ∈ u
⊢ pathComponentIn x F ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨pathComponentIn x u, pathComponentIn_mono huF,
  hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem nonempty_Icc : (Icc a b).Nonempty ↔ a ≤ b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem mul_eq_sum_support_ghas_mul [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
    a * a' =
      ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a',
        DirectSum.of _ _ (GradedMonoid.GMul.mul (a ij.fst) (a' ij.snd))

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a', (of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))

Tactic:
simp only [mul_eq_dfinsupp_sum, DFinsupp.sum, Finset.sum_product]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem conj_smul_subgroupOf {P H : Subgroup G} (hP : P ≤ H) (h : H) :
    MulAut.conj h • P.subgroupOf H = (MulAut.conj (h : G) • P).subgroupOf H

Proof state:
case refine_2
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ (MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H

Tactic:
rintro p ⟨g, hg, hp⟩

Result:
case refine_2.intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h p : ↥H
g : G
hg : g ∈ ↑P
hp : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g = H.subtype p
⊢ p ∈ MulAut.conj h • P.subgroupOf H

Proof state:
case refine_2.intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h p : ↥H
g : G
hg : g ∈ ↑P
hp : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g = H.subtype p
⊢ p ∈ MulAut.conj h • P.subgroupOf H

Tactic:
exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h g : ↥H
hg : g ∈ ↑(P.subgroupOf H)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut ↥H) ↥H) (MulAut.conj h)) g ∈ (MulAut.conj ↑h • P).subgroupOf H

Tactic:
exact ⟨g, hg, rfl⟩

Result:
no goals

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

Tactic:
rintro - ⟨g, hg, rfl⟩

Result:
case refine_1.intro.intro
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h g : ↥H
hg : g ∈ ↑(P.subgroupOf H)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut ↥H) ↥H) (MulAut.conj h)) g ∈ (MulAut.conj ↑h • P).subgroupOf H

Proof state:
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

case refine_2
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ (MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_left_iff_of_base_lt_one (hx0 : 0 < x) (hx1 : x < 1) :
    x ^ y ≤ x ^ z ↔ z ≤ y

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
  mul_le_mul_right_of_neg (log_neg hx0 hx1)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_add_one_of_ne_neg_one {A : M} : ∀ n : ℤ, n ≠ -1 → A ^ (n + 1) = A ^ n * A
  | (n : ℕ), _ => by simp only [pow_succ, ← Nat.cast_succ, zpow_natCast]
  | -1, h => absurd rfl h
  | -((n : ℕ) + 2), _ => by
    rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
    · apply zpow_add_one (isUnit_det_of_left_inverse h)
    · show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A
      simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_mul]

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

Tactic:
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)

Result:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

Proof state:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A

Tactic:
simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_mul]

Result:
no goals

Proof state:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

Tactic:
apply zpow_add_one (isUnit_det_of_left_inverse h)

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : ↑n ≠ -1
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
simp only [pow_succ, ← Nat.cast_succ, zpow_natCast]

Result:
no goals

Proof state:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

Tactic:
show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A

Result:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Icc : (fun x => x - a) '' Icc b c = Icc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Icc b c = Icc (b - a) (c - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.integralRep_mem_nonZeroDivisors
    {I : FractionalIdeal R⁰ (FractionRing R)} (hI : I ≠ 0) :
    I.num ∈ (Ideal R)⁰

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
⊢ I.num ∈ (Ideal R)⁰

Tactic:
rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredPrelimit_iff_exists_covBy (a : α) : ¬IsPredPrelimit a ↔ ∃ b, a ⋖ b

Proof state:
α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsPredPrelimit a ↔ ∃ b, a ⋖ b

Tactic:
simp [IsPredPrelimit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k : α} :
    (m.erase k).getKey! k = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
k : α
⊢ (m.erase k).getKey! k = default

Tactic:
simp_to_model [erase] using List.getKey!_eraseKey_self

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Topology.IsInducing.hasProd_iff [CommMonoid γ] [TopologicalSpace γ] {G}
    [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) (a : α) :
    HasProd (g ∘ f) (g a) ↔ HasProd f a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) ↔ HasProd f a

Tactic:
simp_rw [HasProd, comp_apply, ← map_prod]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s => g (∏ x ∈ s, f x)) atTop (𝓝 (g a)) ↔ Tendsto (fun s => ∏ x ∈ s, f x) atTop (𝓝 a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s => g (∏ x ∈ s, f x)) atTop (𝓝 (g a)) ↔ Tendsto (fun s => ∏ x ∈ s, f x) atTop (𝓝 a)

Tactic:
exact hg.tendsto_nhds_iff.symm

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
lemma torsion_int {G} [AddCommGroup G] :
    (torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G

Proof state:
case h
G : Type u_3
inst✝ : AddCommGroup G
x : G
⊢ (∃ n, n ≠ 0 ∧ n • x = 0) ↔ x ∈ (torsion ℤ G).toAddSubgroup

Tactic:
simp [mem_nonZeroDivisors_iff_ne_zero]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : AddCommGroup G
⊢ (torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G

Tactic:
ext x

Result:
case h
G : Type u_3
inst✝ : AddCommGroup G
x : G
⊢ x ∈ (torsion ℤ G).toAddSubgroup ↔ x ∈ AddCommGroup.torsion G

Proof state:
case h
G : Type u_3
inst✝ : AddCommGroup G
x : G
⊢ x ∈ (torsion ℤ G).toAddSubgroup ↔ x ∈ AddCommGroup.torsion G

Tactic:
refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm

Result:
case h
G : Type u_3
inst✝ : AddCommGroup G
x : G
⊢ (∃ n, n ≠ 0 ∧ n • x = 0) ↔ x ∈ (torsion ℤ G).toAddSubgroup
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_ite_mem (s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
⊢ (∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem isOpen_lt [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsOpen { b | f b < g b }

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalSpace β
f g : β → α
hf : Continuous f
hg : Continuous g
⊢ IsOpen {b | f b < g b}

Tactic:
simpa only [lt_iff_not_le] using (isClosed_le hg hf).isOpen_compl

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_lt' : a⁻¹ < b ↔ b⁻¹ < a

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem Ideal.mem_prime_of_mul_mem_pow [IsDedekindDomain S] {P : Ideal S} [P_prime : P.IsPrime]
    (hP : P ≠ ⊥) {i : ℕ} {a b : S} (a_not_mem : a ∉ P ^ (i + 1)) (ab_mem : a * b ∈ P ^ (i + 1)) :
    b ∈ P

Proof state:
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
a b : S
a_not_mem : a ∉ P ^ (i + 1)
ab_mem : a * b ∈ P ^ (i + 1)
⊢ b ∈ P

Tactic:
simp only [← Ideal.span_singleton_le_iff_mem, ← Ideal.dvd_iff_le, pow_succ, ←
  Ideal.span_singleton_mul_span_singleton] at a_not_mem ab_mem ⊢

Result:
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
a b : S
a_not_mem : ¬P ^ i * P ∣ span {a}
ab_mem : P ^ i * P ∣ span {a} * span {b}
⊢ P ∣ span {b}

Proof state:
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
a b : S
a_not_mem : ¬P ^ i * P ∣ span {a}
ab_mem : P ^ i * P ∣ span {a} * span {b}
⊢ P ∣ span {b}

Tactic:
exact (prime_pow_succ_dvd_mul (Ideal.prime_of_isPrime hP P_prime) ab_mem).resolve_left a_not_mem

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_X_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : W.add P Q = addZ P Q •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.add P Q =
    addZ P Q •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
rw [add, if_neg <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
lemma of_isEquivalence (L : C ⥤ D) (W : MorphismProperty C)
    (hW : W ≤ MorphismProperty.isomorphisms C) [IsEquivalence L] :
    L.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
hW : W ≤ MorphismProperty.isomorphisms C
inst✝ : L.IsEquivalence
⊢ L.IsLocalization W

Tactic:
haveI : (𝟭 C).IsLocalization W := for_id W hW

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
hW : W ≤ MorphismProperty.isomorphisms C
inst✝ : L.IsEquivalence
this : (𝟭 C).IsLocalization W
⊢ L.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
hW : W ≤ MorphismProperty.isomorphisms C
inst✝ : L.IsEquivalence
this : (𝟭 C).IsLocalization W
⊢ L.IsLocalization W

Tactic:
exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem bot_of_map_eq_bot {I : LieIdeal R L} (h₁ : Function.Injective f) (h₂ : I.map f = ⊥) :
    I = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥

Tactic:
exact h₂

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥

Tactic:
rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : Function.Injective ⇑f
h₂ : map f I = ⊥
⊢ I = ⊥

Tactic:
rw [← f.ker_eq_bot, LieHom.ker] at h₁

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥
-- Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
lemma equiv_shift' {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
    (f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
    SmallHom.equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫
      (SmallHom.equiv W L f)⟦n⟧' ≫ ((L.commShiftIso a).hom.app Y)⟦n⟧' ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y

Proof state:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (SmallHom.equiv W L) (f.shift n a' h) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫
          (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y

Tactic:
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc,
  L.commShiftIso_add' h, Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc,
  ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
  | .head l => ⟨[], l, rfl⟩
  | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩

Proof state:
α : Type u_1
a : α
l : List α
b : α
as✝ : List α
h : Mem a as✝
s t : List α
h' : as✝ = s ++ a :: t
⊢ b :: as✝ = b :: s ++ a :: t

Tactic:
rw [h', cons_append]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem closure_eq_inter_uniformity {t : Set (α × α)} : closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d) :=
  calc
    closure t = ⋂ (V) (_ : V ∈ 𝓤 α ∧ SymmetricRel V), V ○ t ○ V := closure_eq_uniformity t
    _ = ⋂ V ∈ 𝓤 α, V ○ t ○ V :=
      Eq.symm <|
        UniformSpace.hasBasis_symmetric.biInter_mem fun _ _ hV =>
          compRel_mono (compRel_mono hV Subset.rfl) hV
    _ = ⋂ V ∈ 𝓤 α, V ○ (t ○ V)

Proof state:
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
⊢ ⋂ V ∈ 𝓤 α, V ○ t ○ V = ⋂ V ∈ 𝓤 α, V ○ (t ○ V)

Tactic:
simp only [compRel_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
theorem isGalois_iff_pretransitive (X : C) [IsConnected X] :
    IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ Nonempty (Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).carrier)) ↔
    MulAction.IsPretransitive (Aut X) (F.obj X).carrier

Tactic:
exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X).carrier

Tactic:
rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ Nonempty (Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).carrier)) ↔
    MulAction.IsPretransitive (Aut X) (F.obj X).carrier
-- Mathlib/Data/Finsupp/Order.lean
lemma mapDomain_nonpos (hg : g ≤ 0) : g.mapDomain f ≤ 0

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : OrderedAddCommMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
simpa using mapDomain_mono hg

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp) nsmul_empty]
lemma empty_pow (hn : n ≠ 0) : (∅ : Set α) ^ n = ∅ := match n with | n + 1 => by simp [pow_succ]

Proof state:
α : Type u_2
inst✝ : Monoid α
n✝ n : ℕ
hn : n + 1 ≠ 0
⊢ ∅ ^ (n + 1) = ∅

Tactic:
simp [pow_succ]

Result:
no goals