harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.exists_nonzero_dvd
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ r : R, r ≠ 0 ∧ s ∣ algebraMap R S r

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ (aeval s) (q - C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ (aeval s) (q - C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : s ∣ (algebraMap R S) (q.coeff 0)
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : s ∣ (algebraMap R S) (q.coeff 0)
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
exact ⟨q.coeff 0, hq0, key⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem card_Ico_eq_card_Icc_sub_one (a b : α) : #(Ico a b) = #(Icc a b) - 1

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
by_cases h : a ≤ b

Result:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

Proof state:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
rw [Icc_eq_cons_Ico h, card_cons]

Result:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1

Proof state:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem pow_four [Infinite R] : #R ^ 4 = #R :=
  power_nat_eq (aleph0_le_mk R) <| by decide

Proof state:
R : Type u_1
inst✝ : Infinite R
⊢ 1 ≤ 4

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α → Option β) :
    filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

Proof state:
case mk
α : Type u_1
β : Type u_2
l' : Array α
f : α → Option β
toList✝ : List α
⊢ filterMap f ({ toList := toList✝ } ++ l') = filterMap f { toList := toList✝ } ++ filterMap f l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝¹ toList✝ : List α
⊢ filterMap f ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    filterMap f { toList := toList✝¹ } ++ filterMap f { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
l l' : Array α
f : α → Option β
⊢ filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
l' : Array α
f : α → Option β
toList✝ : List α
⊢ filterMap f ({ toList := toList✝ } ++ l') = filterMap f { toList := toList✝ } ++ filterMap f l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝¹ toList✝ : List α
⊢ filterMap f ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    filterMap f { toList := toList✝¹ } ++ filterMap f { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factorSet_some {p : Associates α} {hp : Irreducible p}
    {l : Multiset { a : Associates α // Irreducible a }} :
    p ∈ (l : FactorSet α) ↔ Subtype.mk p hp ∈ l

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ (if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ↑l else False) ↔ l.Mem ⟨p, hp⟩

Tactic:
split_ifs

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem ⟨p, hp⟩ ↑l ↔ l.Mem ⟨p, hp⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ FactorSetMem (↑l) p ↔ l.Mem ⟨p, hp⟩

Tactic:
dsimp only [FactorSetMem]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ (if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ↑l else False) ↔ l.Mem ⟨p, hp⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem ⟨p, hp⟩ ↑l ↔ l.Mem ⟨p, hp⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l

Tactic:
dsimp only [Membership.mem]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ FactorSetMem (↑l) p ↔ l.Mem ⟨p, hp⟩
-- Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
lemma SpecMap_iff {R S : CommRingCat} {φ : R ⟶ S} :
    IsIntegralHom (Spec.map φ) ↔ φ.hom.IsIntegral

Proof state:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]

Result:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔ (CommRingCat.Hom.hom φ).IsIntegral

R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S)

Proof state:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔ (CommRingCat.Hom.hom φ).IsIntegral

R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S)

Tactic:
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
  (arrowIsoΓSpecOfIsAffine φ).symm, inferInstance]

Result:
no goals

Proof state:
R S : CommRingCat
φ : R ⟶ S
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso

Result:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = []

Proof state:
α : Type u_1
xs✝ : List α
x : α
xs : List α
⊢ (x :: xs).reverse = [] ↔ x :: xs = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ [].reverse = [] ↔ [] = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.reverse = [] ↔ xs = []

Tactic:
match xs with
| [] => simp
| x :: xs => simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_ofNat (n : ℕ) : W.ΨSq n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.ΨSq ↑n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1

Tactic:
simp only [ΨSq, preΨ_ofNat, Int.even_coe_nat]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp] lemma natDegree_X_mul (hp : p ≠ 0) : natDegree (X * p) = natDegree p + 1

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ (X * p).natDegree = p.natDegree + 1

Tactic:
rw [commute_X p, natDegree_mul_X hp]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem _root_.IsAntichain.ordConnected (hs : IsAntichain (· ≤ ·) s) : s.OrdConnected :=
  ⟨fun x hx y hy z hz => by
    obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
    rw [Icc_self, mem_singleton_iff] at hz
    rwa [hz]⟩

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s

Tactic:
rwa [hz]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s

Tactic:
rw [Icc_self, mem_singleton_iff] at hz

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ioc' (ha : μ {a} ≠ ∞) :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b

Tactic:
contrapose! hab

Result:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a < b
⊢ a ≤ b

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
by_cases hab : a ≤ b

Result:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a < b
⊢ a ≤ b

Tactic:
exact hab.le

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [Icc_eq_empty hab, Ioc_eq_empty]

Result:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [← Ioc_union_left hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr ha.lt_top), and_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α} [Inhabited β]
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    get! (ofList l) k = default

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : LawfulBEq α
l : List (α × β)
k : α
inst✝ : Inhabited β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ get! (ofList l) k = default

Tactic:
simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_norm_rpow_iff {f : α → β} {p : ℝ≥0∞}
    (hf : AEStronglyMeasurable f μ) (p_zero : p ≠ 0) (p_top : p ≠ ∞) :
    Integrable (fun x : α => ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ

Tactic:
rw [← memLp_norm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
  ENNReal.div_self p_zero p_top]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.sSup_mem_of_nonempty (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty)
    (hts : t ⊆ s) : sSup t ∈ s

Proof state:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
⊢ sSup t ∈ s

Tactic:
have := ht.to_subtype

Result:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Proof state:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ∀ (i : ↑t), ↑i ∈ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ sSup t ∈ s

Tactic:
rw [sSup_eq_iSup']

Result:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s

Proof state:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty (by simpa)

Result:
no goals

Proof state:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Tactic:
have := ht'.to_subtype

Result:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ sSup t ∈ s
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq (f : α → E) (hf : Integrable f μ) : ∫ a, f a ∂μ = L1.integral (hf.toL1 f)

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = L1.integral (Integrable.toL1 f hf)

Tactic:
simp [integral, hE, hf]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_closedBall [∀ i, MetricSpace (α i)] (x : ∀ i, α i) {r : ℝ} (hr : 0 ≤ r) :
    Measure.pi μ (Metric.closedBall x r) = ∏ i, μ i (Metric.closedBall (x i) r)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (Metric.closedBall x r) = ∏ i : ι, (μ i) (Metric.closedBall (x i) r)

Tactic:
rw [closedBall_pi _ hr, pi_pi]

Result:
no goals
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_eq_discr_of_algEquiv [Fintype ι] (b : ι → B) (f : B ≃ₐ[A] C) :
    Algebra.discr A b = Algebra.discr A (f ∘ b)

Proof state:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr A (⇑f ∘ b)

Tactic:
congr

Result:
case e_M
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ traceMatrix A b = traceMatrix A (⇑f ∘ b)

Proof state:
case e_M.a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i✝ j✝ : ι
⊢ traceMatrix A b i✝ j✝ = traceMatrix A (⇑f ∘ b) i✝ j✝

Tactic:
simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]

Result:
no goals

Proof state:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ discr A b = discr A (⇑f ∘ b)

Tactic:
rw [discr_def]

Result:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr A (⇑f ∘ b)

Proof state:
case e_M
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ traceMatrix A b = traceMatrix A (⇑f ∘ b)

Tactic:
ext

Result:
case e_M.a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i✝ j✝ : ι
⊢ traceMatrix A b i✝ j✝ = traceMatrix A (⇑f ∘ b) i✝ j✝
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_sumElim {f : X → Z} {g : Y → Z} :
    IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Tactic:
simp only [isOpenMap_sum, elim_inl, elim_inr]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : a ^ 4 + b ^ 4 ≠ c ^ 2

Proof state:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : a ^ 4 + b ^ 4 = c ^ 2
⊢ False

Tactic:
obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ :=
  Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))

Result:
case intro.intro.intro.intro.intro
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : a ^ 4 + b ^ 4 = c ^ 2
a0 b0 c0 : ℤ
hf : Fermat42.Minimal a0 b0 c0
h2 : a0 % 2 = 1
hp : 0 < c0
⊢ False

Proof state:
case intro.intro.intro.intro.intro
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : a ^ 4 + b ^ 4 = c ^ 2
a0 b0 c0 : ℤ
hf : Fermat42.Minimal a0 b0 c0
h2 : a0 % 2 = 1
hp : 0 < c0
⊢ False

Tactic:
apply Fermat42.not_minimal hf h2 hp

Result:
no goals

Proof state:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a ^ 4 + b ^ 4 ≠ c ^ 2

Tactic:
intro h

Result:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : a ^ 4 + b ^ 4 = c ^ 2
⊢ False
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem finite_compl_fixedBy_swap {x y : α} : (fixedBy α (swap x y))ᶜ.Finite :=
  Set.Finite.subset (s := {x, y}) (by simp)
    (compl_subset_comm.mp fun z h ↦ by apply swap_apply_of_ne_of_ne <;> rintro rfl <;> simp at h)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x y z : α
h : z ∈ {x, y}ᶜ
⊢ z ∈ fixedBy α (swap x y)

Tactic:
apply swap_apply_of_ne_of_ne <;> rintro rfl <;> simp at h

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x y : α
⊢ {x, y}.Finite

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem pow {w : σ → M} (hφ : IsWeightedHomogeneous w φ m) (n : ℕ) :
    IsWeightedHomogeneous w (φ ^ n) (n • m)

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous w 1 0

Tactic:
exact isWeightedHomogeneous_one R w

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)

Tactic:
rw [pow_succ, succ_nsmul]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous w (φ ^ 0) (0 • m)

Tactic:
rw [pow_zero, zero_smul]

Result:
case zero
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous w 1 0

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)

Tactic:
exact ih.mul hφ

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
⊢ IsWeightedHomogeneous w (φ ^ n) (n • m)

Tactic:
induction n with
| zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
| succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ

Result:
no goals