harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Divisors.lean
theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n.Prime

Proof state:
case refine_1.refine_1
n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n

Tactic:
match n with
| 0 => contradiction
| 1 => contradiction
| Nat.succ (Nat.succ n) => simp [succ_le_succ]

Result:
no goals

Proof state:
n : ℕ
h : properDivisors 0 = {1}
⊢ 2 ≤ 0

Tactic:
contradiction

Result:
no goals

Proof state:
case refine_1.refine_2.refine_1
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n

Tactic:
by_contra!

Result:
case refine_1.refine_2.refine_1
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False

Proof state:
case refine_1.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n

Tactic:
rw [← mem_singleton, ← h, mem_properDivisors]

Result:
case refine_1.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n

Proof state:
case refine_1.refine_2.refine_1
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False

Tactic:
simp only [nonpos_iff_eq_zero.mp this, this] at h

Result:
case refine_1.refine_2.refine_1
n m : ℕ
hdvd : m ∣ n
this : n ≤ 0
h : properDivisors 0 = {1}
⊢ False

Proof state:
case refine_1
n : ℕ
h : n.properDivisors = {1}
⊢ Prime n

Tactic:
refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩

Result:
case refine_1.refine_1
n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n

case refine_1.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n

Proof state:
case refine_1.refine_2.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n

Tactic:
simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm

Result:
no goals

Proof state:
case refine_2
n : ℕ
⊢ Prime n → n.properDivisors = {1}

Tactic:
exact fun h => Prime.properDivisors h

Result:
no goals

Proof state:
case refine_1
n : ℕ
⊢ n.properDivisors = {1} → Prime n

Tactic:
intro h

Result:
case refine_1
n : ℕ
h : n.properDivisors = {1}
⊢ Prime n

Proof state:
n✝ n : ℕ
h : n.succ.succ.properDivisors = {1}
⊢ 2 ≤ n.succ.succ

Tactic:
simp [succ_le_succ]

Result:
no goals

Proof state:
case refine_1.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n

Tactic:
have := Nat.le_of_dvd ?_ hdvd

Result:
case refine_1.refine_2.refine_2
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n

case refine_1.refine_2.refine_1
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n

Proof state:
n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
n : ℕ
⊢ n.properDivisors = {1} → Prime n

case refine_2
n : ℕ
⊢ Prime n → n.properDivisors = {1}

Proof state:
n : ℕ
h : properDivisors 1 = {1}
⊢ 2 ≤ 1

Tactic:
contradiction

Result:
no goals

Proof state:
case refine_1.refine_2.refine_1
n m : ℕ
hdvd : m ∣ n
this : n ≤ 0
h : properDivisors 0 = {1}
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma measure_mutuallySingularSetSlice (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
    (a : α) :
    η a (mutuallySingularSetSlice κ η a) = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
x : γ
hx : 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ MeasurableSet {x | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}

Tactic:
exact (measurableSet_singleton 0).preimage (by fun_prop)

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} = 0

Tactic:
simp_rw [ofNNReal_toNNReal]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (((κ + η).withDensity fun a x => ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) a)
      {x | 1 ≤ κ.rnDerivAux (κ + η) a x} =
    0
-- Mathlib/Data/Set/Card.lean
lemma one_lt_ncard_of_nonempty_of_even (hs : Set.Finite s) (hn : Set.Nonempty s

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam s.Nonempty _auto✝
he : Even s.ncard
⊢ 1 < s.ncard

Tactic:
rw [← Set.ncard_pos hs] at hn

Result:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam (0 < s.ncard) _auto✝
he : Even s.ncard
⊢ 1 < s.ncard

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam (0 < s.ncard) _auto✝
he : Even s.ncard
this : s.ncard ≠ 1
⊢ 1 < s.ncard

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam (0 < s.ncard) _auto✝
he : Even s.ncard
h : s.ncard = 1
⊢ False

Tactic:
simp [h] at he

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam (0 < s.ncard) _auto✝
he : Even s.ncard
⊢ 1 < s.ncard

Tactic:
have : s.ncard ≠ 1 := fun h ↦ by simp [h] at he

Result:
α : Type u_1
s : Set α
hs : s.Finite
hn : autoParam (0 < s.ncard) _auto✝
he : Even s.ncard
this : s.ncard ≠ 1
⊢ 1 < s.ncard
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharTwoJEqZeroNF_of_char_two : W.c₆ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -216 * W.b₆ = 0

Tactic:
linear_combination -108 * W.b₆ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ W.c₆ = 0

Tactic:
rw [c₆_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -216 * W.b₆ = 0
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mul_mk'_one_eq_mk' (x) (y : S) : f.toMap x * f.mk' 1 y = f.mk' x y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.toMap x * f.mk' 1 y = f.mk' x y

Tactic:
rw [mul_mk'_eq_mk'_of_mul, mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_eq_empty_iff {f : α → M} : mulSupport f = ∅ ↔ f = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
⊢ mulSupport f = ∅ ↔ f = 1

Tactic:
rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]

Result:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
⊢ (∀ x ∉ ∅, f x = 1) ↔ ∀ (x : α), f x = 1 x

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
⊢ (∀ x ∉ ∅, f x = 1) ↔ ∀ (x : α), f x = 1 x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem zero_smul (x : X[S⁻¹]) : (0 : R[S⁻¹]) • x = 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ ↑1 * 0 = 0 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
x : OreLocalization S X
⊢ 0 • x = 0

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • (r /ₒ s) = 0

Proof state:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • (r /ₒ s) = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_smul_char 0 r 1 s 0 1 (by simp)]

Result:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • r /ₒ (1 * 1) = 0

Proof state:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • r /ₒ (1 * 1) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem isPeriodicPt_minimalPeriod (f : α → α) (x : α) : IsPeriodicPt f (minimalPeriod f x) x

Proof state:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
delta minimalPeriod

Result:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x

Proof state:
case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
exact isPeriodicPt_zero f x

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x

Tactic:
split_ifs with hx

Result:
case pos
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Proof state:
case pos
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

Tactic:
exact (Nat.find_spec hx).2

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_mul_of_coprime' {a b : Associates α} {p : Associates α}
    (hp : Irreducible p) (hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) :
    count p (a * b).factors = count p a.factors ∨ count p (a * b).factors = count p b.factors

Proof state:
case neg.inr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors

Tactic:
apply Or.intro_left

Result:
case neg.inr.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_def [DecidableEq σ] (n : σ) (p : MvPolynomial σ R) :
    p.degreeOf n = p.degrees.count n

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ degreeOf n p = Multiset.count n p.degrees

Tactic:
rw [degreeOf]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
n : σ
p : MvPolynomial σ R
⊢ Multiset.count n p.degrees = Multiset.count n p.degrees

Tactic:
convert rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma rightUnshift_v {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n)
    (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p + n' = p') :
    (γ.rightUnshift n hn).v p q hpq = γ.v p p' hp' ≫
      (L.shiftFunctorObjXIso a p' q (by rw [← hpq, ← hn, ← add_assoc, hp'])).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (mk fun p q hpq => γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom).v p q hpq =
    γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom

Tactic:
simp only [mk_v]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ q = p' + a

Tactic:
rw [← hpq, ← hn, ← add_assoc, hp']

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ (γ.rightUnshift n hn).v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a p' q ⋯).hom

Tactic:
subst hp'

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (γ.rightUnshift n hn).v p q hpq = γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (γ.rightUnshift n hn).v p q hpq = γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom

Tactic:
dsimp only [rightUnshift]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (mk fun p q hpq => γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom).v p q hpq =
    γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem isPrime_of_isPrime_prod_top {I : Ideal R} (h : (Ideal.prod I (⊤ : Ideal S)).IsPrime) :
    I.IsPrime

Proof state:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ := by
  rw [Prod.mk_mul_mk, mul_one, mem_prod]
  exact ⟨hxy, trivial⟩

Result:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ I.prod ⊤
⊢ x ∈ I ∨ y ∈ I

Proof state:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I ≠ ⊤

Tactic:
contrapose! h

Result:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(I.prod ⊤).IsPrime

Proof state:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ I.prod ⊤
⊢ x ∈ I ∨ y ∈ I

Tactic:
simpa using h.mem_or_mem this

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I.IsPrime

Tactic:
constructor

Result:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I ≠ ⊤

case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Proof state:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(I.prod ⊤).IsPrime

Tactic:
rw [h, prod_top_top, isPrime_iff]

Result:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ x * y ∈ I ∧ 1 ∈ ⊤

Tactic:
exact ⟨hxy, trivial⟩

Result:
no goals

Proof state:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
intro x y hxy

Result:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Proof state:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)

Tactic:
simp [isPrime_iff, h]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x, 1) * (y, 1) ∈ I.prod ⊤

Tactic:
rw [Prod.mk_mul_mk, mul_one, mem_prod]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ x * y ∈ I ∧ 1 ∈ ⊤
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma targetAffineLocally_affineAnd_eq_affineLocally (hQ : RingHom.PropertyIsLocal Q) :
    targetAffineLocally (affineAnd Q) =
      (@IsAffineHom ⊓ @affineLocally Q : MorphismProperty Scheme.{u})

Proof state:
case h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
exact targetAffineLocally_affineAnd_iff_affineLocally hQ f

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) =
    @IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] => Q

Tactic:
ext X Y f

Result:
case h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] => Q) f
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) :
    Tendsto (fun x : ℝ => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0)

Proof state:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x => |x| ^ s * rexp (-a * |x| ^ 2)) (cocompact ℝ) (𝓝 0)

Tactic:
erw [cocompact_eq_atBot_atTop, ← comap_abs_atTop,
  @tendsto_comap'_iff _ _ _ (fun y => y ^ s * rexp (-a * y ^ 2)) _ _ _
    (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]

Result:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun y => y ^ s * rexp (-a * y ^ 2)) atTop (𝓝 0)

Proof state:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun y => y ^ s * rexp (-a * y ^ 2)) atTop (𝓝 0)

Tactic:
exact
  (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
    (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

Result:
no goals

Proof state:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0)

Tactic:
conv in rexp _ => rw [← sq_abs]

Result:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x => |x| ^ s * rexp (-a * |x| ^ 2)) (cocompact ℝ) (𝓝 0)
-- Mathlib/Topology/SeparatedMap.lean
lemma Continuous.mapPullback {X₁ X₂ Y₁ Y₂ Z₁ Z₂}
    [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z₁] [TopologicalSpace Z₂]
    {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂}
    {mapX : X₁ → X₂} (contX : Continuous mapX) {mapY : Y₁ → Y₂}
    {mapZ : Z₁ → Z₂} (contZ : Continuous mapZ)
    {commX : f₂ ∘ mapX = mapY ∘ f₁} {commZ : g₂ ∘ mapZ = mapY ∘ g₁} :
    Continuous (Function.mapPullback mapX mapY mapZ commX commZ)

Proof state:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Z₁
inst✝ : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous (Function.mapPullback mapX mapY mapZ commX commZ)

Tactic:
refine continuous_induced_rng.mpr (continuous_prod_mk.mpr ⟨?_, ?_⟩) <;>
apply_rules [continuous_fst, continuous_snd, continuous_subtype_val, Continuous.comp]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem length_alternatingWord (i i' : B) (m : ℕ) :
    List.length (alternatingWord i i' m) = m

Proof state:
B : Type u_1
i i' : B
m : ℕ
⊢ (alternatingWord i i' m).length = m

Tactic:
induction' m with m ih generalizing i i'

Result:
case zero
B : Type u_1
i i' : B
⊢ (alternatingWord i i' 0).length = 0

case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), (alternatingWord i i' m).length = m
i i' : B
⊢ (alternatingWord i i' (m + 1)).length = m + 1

Proof state:
case zero
B : Type u_1
i i' : B
⊢ (alternatingWord i i' 0).length = 0

Tactic:
dsimp [alternatingWord]

Result:
no goals

Proof state:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), (alternatingWord i i' m).length = m
i i' : B
⊢ (alternatingWord i i' (m + 1)).length = m + 1

Tactic:
simpa [alternatingWord] using ih i' i

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0

Proof state:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
h : ¬p head = true
⊢ (bif p head then n + 1 + countP.go p tail 0 else n + countP.go p tail 0) =
    n + bif p head then 1 + countP.go p tail 0 else countP.go p tail 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
⊢ countP.go p (head :: tail) n = n + countP.go p (head :: tail) 0

Tactic:
unfold countP.go

Result:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
⊢ (bif p head then countP.go p tail (n + 1) else countP.go p tail n) =
    n + bif p head then countP.go p tail (0 + 1) else countP.go p tail 0

Proof state:
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
h : p head = true
⊢ (bif p head then n + 1 + countP.go p tail 0 else n + countP.go p tail 0) =
    n + bif p head then 1 + countP.go p tail 0 else countP.go p tail 0

Tactic:
simp [h, Nat.add_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
n : Nat
⊢ countP.go p [] n = n + countP.go p [] 0

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
⊢ (bif p head then n + 1 + countP.go p tail 0 else n + countP.go p tail 0) =
    n + bif p head then 1 + countP.go p tail 0 else countP.go p tail 0

Tactic:
if h : p head then simp [h, Nat.add_assoc] else simp [h]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
⊢ (bif p head then countP.go p tail (n + 1) else countP.go p tail n) =
    n + bif p head then countP.go p tail (0 + 1) else countP.go p tail 0

Tactic:
rw [ih (n := n + 1), ih (n := n), ih (n := 1)]

Result:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : ∀ {n : Nat}, countP.go p tail n = n + countP.go p tail 0
n : Nat
⊢ (bif p head then n + 1 + countP.go p tail 0 else n + countP.go p tail 0) =
    n + bif p head then 1 + countP.go p tail 0 else countP.go p tail 0

Proof state:
α : Type u_1
p : α → Bool
n : Nat
l : List α
⊢ countP.go p l n = n + countP.go p l 0

Tactic:
induction l generalizing n with
| nil => rfl
| cons head tail ih =>
  unfold countP.go
  rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
  if h : p head then simp [h, Nat.add_assoc] else simp [h]

Result:
no goals