harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Flat/Basic.lean
theorem includeLeft_injective [Module.Flat R A] (hb : Function.Injective (algebraMap R B)) :
    Function.Injective (includeLeft : A →ₐ[S] A ⊗[R] B)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ ⇑includeLeft = ⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm

Tactic:
ext

Result:
case h.e'_3.h
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
x✝ : A
⊢ includeLeft x✝ = (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm) x✝

Proof state:
case h.e'_3.h
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
x✝ : A
⊢ includeLeft x✝ = (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ Function.Injective ⇑includeLeft

Tactic:
convert Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb
  |>.comp (_root_.TensorProduct.rid R A).symm.injective

Result:
case h.e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ ⇑includeLeft = ⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    (map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
rw [map_toPoly,
  eq_prod_roots_of_splits <|
    (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
  leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * (Multiset.map (fun a => X - C a) {x, y, z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]

Result:
no goals

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * (Multiset.map (fun a => X - C a) {x, y, z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem prod_single_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {i : ι} {b : β i} {h : ∀ i, β i → γ} (h_zero : h i 0 = 1) : (single i b).prod h = h i b

Proof state:
case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
simp [DFinsupp.prod, support_single_ne_zero h]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
⊢ (single i b).prod h = h i b

Tactic:
by_cases h : b ≠ 0

Result:
case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

Proof state:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
rw [not_not] at h

Result:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ (single i b).prod h✝ = h✝ i b

Proof state:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1

Tactic:
rfl

Result:
no goals

Proof state:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
simp [h, prod_zero_index, h_zero]

Result:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem base_mul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts f) : C (f r) * p ∈ lifts f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : p ∈ lifts f
⊢ C (f r) * p ∈ lifts f

Tactic:
simp only [lifts, RingHom.mem_rangeS] at hp ⊢

Result:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, (mapRingHom f) x = p
⊢ ∃ x, (mapRingHom f) x = C (f r) * p

Proof state:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ (mapRingHom f) (C r * p₁) = C (f r) * (mapRingHom f) p₁

Tactic:
simp only [coe_mapRingHom, map_C, map_mul]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ∃ x, (mapRingHom f) x = C (f r) * (mapRingHom f) p₁

Tactic:
use C r * p₁

Result:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ (mapRingHom f) (C r * p₁) = C (f r) * (mapRingHom f) p₁

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, (mapRingHom f) x = p
⊢ ∃ x, (mapRingHom f) x = C (f r) * p

Tactic:
obtain ⟨p₁, rfl⟩ := hp

Result:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ∃ x, (mapRingHom f) x = C (f r) * (mapRingHom f) p₁
-- Mathlib/Data/List/FinRange.lean
theorem nodup_ofFn_ofInjective {n} {f : Fin n → α} (hf : Function.Injective f) :
    Nodup (ofFn f)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup

Tactic:
rw [ofFn_eq_pmap]

Result:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (pmap (fun i hi => f ⟨i, hi⟩) (range n) ⋯).Nodup

Proof state:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (pmap (fun i hi => f ⟨i, hi⟩) (range n) ⋯).Nodup

Tactic:
exact (nodup_range n).pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem Ici_sSup (S : Set α) : Ici (sSup S) = ⨆ a ∈ S, Ici a :=
  SetLike.ext fun c => by simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
S : Set α
c : α
⊢ c ∈ Ici (sSup S) ↔ c ∈ ⨆ a ∈ S, Ici a

Tactic:
simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]

Result:
no goals
-- Mathlib/GroupTheory/Solvable.lean
theorem IsSolvable.commutator_lt_top_of_nontrivial [hG : IsSolvable G] [Nontrivial G] :
    commutator G < ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G ≠ ⊤

Tactic:
obtain ⟨n, hn⟩ := hG

Result:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ _root_.commutator G ≠ ⊤

Proof state:
case mk.intro.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
⊢ derivedSeries G 0 = ⊤

Tactic:
exact derivedSeries_zero G

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G < ⊤

Tactic:
rw [lt_top_iff_ne_top]

Result:
G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G ≠ ⊤

Proof state:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n ≠ ⊥

Tactic:
refine ne_of_eq_of_ne ?_ top_ne_bot

Result:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n = ⊤

Proof state:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n = ⊤

Tactic:
induction' n with n h

Result:
case mk.intro.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
⊢ derivedSeries G 0 = ⊤

case mk.intro.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
n : ℕ
h : derivedSeries G n = ⊤
⊢ derivedSeries G (n + 1) = ⊤

Proof state:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ _root_.commutator G ≠ ⊤

Tactic:
contrapose! hn

Result:
case mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : _root_.commutator G = ⊤
⊢ derivedSeries G n ≠ ⊥

Proof state:
case mk.intro.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
n : ℕ
h : derivedSeries G n = ⊤
⊢ derivedSeries G (n + 1) = ⊤

Tactic:
rwa [derivedSeries_succ, h]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem map_id (K : ProperCone ℝ E) : K.map (ContinuousLinearMap.id ℝ E) = K :=
  ProperCone.toPointedCone_injective <| by simpa using IsClosed.closure_eq K.isClosed

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
K : ProperCone ℝ E
⊢ ↑(map (ContinuousLinearMap.id ℝ E) K) = ↑K

Tactic:
simpa using IsClosed.closure_eq K.isClosed

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_powerset (x : PSet) : rank (powerset x) = succ (rank x)

Proof state:
case a
x y✝ : PSet.{u_1}
⊢ y✝ ⊆ x → y✝.rank ≤ x.rank

Tactic:
exact rank_mono

Result:
no goals

Proof state:
case a
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank

Tactic:
simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]

Result:
case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank

Proof state:
case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank

Tactic:
intro

Result:
case a
x y✝ : PSet.{u_1}
⊢ y✝ ⊆ x → y✝.rank ≤ x.rank

Proof state:
case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank

Tactic:
apply rank_lt_of_mem

Result:
case a.a
x : PSet.{u_1}
⊢ x ∈ x.powerset

Proof state:
case a.a
x : PSet.{u_1}
⊢ x ∈ x.powerset

Tactic:
simp

Result:
no goals

Proof state:
case a
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank

Tactic:
rw [succ_le_iff]

Result:
case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank

Proof state:
x : PSet.{u_1}
⊢ x.powerset.rank = succ x.rank

Tactic:
apply le_antisymm

Result:
case a
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank

case a
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem eq_C_of_degree_le_zero (h : degree p ≤ 0) : p = C (coeff p 0)

Proof state:
case a.zero
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = (C (p.coeff 0)).coeff 0

Tactic:
simp

Result:
no goals

Proof state:
case a.succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.degree < ↑(n + 1)

Tactic:
exact h.trans_lt (WithBot.coe_lt_coe.2 n.succ_pos)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p = C (p.coeff 0)

Tactic:
ext (_ | n)

Result:
case a.zero
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = (C (p.coeff 0)).coeff 0

case a.succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)

Proof state:
case a.succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)

Tactic:
rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]

Result:
case a.succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.degree < ↑(n + 1)
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_pow_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
  match n.even_xor_odd with
  | .inl hne => by simp only [*, and_true, ← abs_eq_abs,
    ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]
  | .inr hn => by simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
hne : Even n ∧ ¬Odd n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp only [*, and_true, ← abs_eq_abs,
← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
hn✝ : n ≠ 0
hn : Odd n ∧ ¬Even n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem zpowers_eq_top_of_prime_card {p : ℕ}
    [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : zpowers g = ⊤

Proof state:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : zpowers g = ⊥ ∨ zpowers g = ⊤
⊢ zpowers g = ⊤

Tactic:
rwa [zpowers_eq_bot, or_iff_right hg] at this

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ zpowers g = ⊤

Tactic:
subst h

Result:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
⊢ zpowers g = ⊤

Proof state:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
⊢ zpowers g = ⊤

Tactic:
have := (zpowers g).eq_bot_or_eq_top_of_prime_card

Result:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : zpowers g = ⊥ ∨ zpowers g = ⊤
⊢ zpowers g = ⊤
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma IsSelfAdjoint.sq_spectrumRestricts {a : A} (ha : IsSelfAdjoint a) :
    SpectrumRestricts (a ^ 2) ContinuousMap.realToNNReal

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal

Tactic:
rw [SpectrumRestricts.nnreal_iff, ← cfc_id (R := ℝ) a, ← cfc_pow .., cfc_map_spectrum ..]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ (fun x => id x ^ 2) '' spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ (fun x => id x ^ 2) '' spectrum ℝ a, 0 ≤ x

Tactic:
rintro - ⟨x, -, rfl⟩

Result:
case intro.intro
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ 0 ≤ (fun x => id x ^ 2) x

Proof state:
case intro.intro
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ 0 ≤ (fun x => id x ^ 2) x

Tactic:
exact sq_nonneg x

Result:
no goals
-- Mathlib/Order/Concept.lean
theorem snd_subset_snd_iff : c.snd ⊆ d.snd ↔ d ≤ c

Proof state:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.2 ⊆ d.toProd.2
⊢ extentClosure r d.toProd.2 ⊆ extentClosure r c.toProd.2

Tactic:
exact extentClosure_anti _ h

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.toProd.2 ⊆ d.toProd.2 ↔ d ≤ c

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.2 ⊆ d.toProd.2
⊢ d ≤ c

case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ c.toProd.2 ⊆ d.toProd.2

Proof state:
case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ intentClosure r c.toProd.1 ⊆ intentClosure r d.toProd.1

Tactic:
exact intentClosure_anti _ h

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ c.toProd.2 ⊆ d.toProd.2

Tactic:
rw [← c.closure_fst, ← d.closure_fst]

Result:
case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ intentClosure r c.toProd.1 ⊆ intentClosure r d.toProd.1

Proof state:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.2 ⊆ d.toProd.2
⊢ d ≤ c

Tactic:
rw [← fst_subset_fst_iff, ← c.closure_snd, ← d.closure_snd]

Result:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.2 ⊆ d.toProd.2
⊢ extentClosure r d.toProd.2 ⊆ extentClosure r c.toProd.2
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_liesOver_maximal_of_isIntegral [p.IsMaximal] (B : Type*) [CommRing B]
    [Nontrivial B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] :
    ∃ P : Ideal B, P.IsMaximal ∧ P.LiesOver p

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
p : Ideal A
inst✝⁵ : p.IsMaximal
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver p

Tactic:
obtain ⟨P, hm, hP⟩ := exists_ideal_over_maximal_of_isIntegral (S := B) p <| by simp

Result:
case intro.intro
A : Type u_1
inst✝⁶ : CommRing A
p : Ideal A
inst✝⁵ : p.IsMaximal
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
P : Ideal B
hm : P.IsMaximal
hP : comap (algebraMap A B) P = p
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver p

Proof state:
case intro.intro
A : Type u_1
inst✝⁶ : CommRing A
p : Ideal A
inst✝⁵ : p.IsMaximal
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
P : Ideal B
hm : P.IsMaximal
hP : comap (algebraMap A B) P = p
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver p

Tactic:
exact ⟨P, hm, ⟨hP.symm⟩⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
p : Ideal A
inst✝⁵ : p.IsMaximal
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
⊢ RingHom.ker (algebraMap A B) ≤ p

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_densityProcess_limitProcess (hκν : fst κ ≤ ν)
    [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ x ∂(ν a), Tendsto (fun n ↦ densityProcess κ ν n a x s) atTop
      (𝓝 ((countableFiltration γ).limitProcess
      (fun n x ↦ densityProcess κ ν n a x s) (ν a) x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ = ↑((ν a) univ).toNNReal

Tactic:
rw [ENNReal.coe_toNNReal]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : γ) ∂ν a,
    Tendsto (fun n => κ.densityProcess ν n a x s) atTop
      (𝓝 (Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) x))

Tactic:
refine Submartingale.ae_tendsto_limitProcess (martingale_densityProcess hκν a hs).submartingale
  (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal

Tactic:
refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (ν a) univ = ↑((ν a) univ).toNNReal
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Iio : ((↑) : ℤ → α) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ Int.cast ⁻¹' Iio a = Iio ⌈a⌉

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉

Tactic:
simp [lt_ceil]

Result:
no goals