harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Lattice.lean
theorem inter_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∩ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ∩ t i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j

Tactic:
simp only [inter_iUnion]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem finite_iff_finite_of_encard_eq_encard (h : s.encard = t.encard) : s.Finite ↔ t.Finite

Proof state:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Finite ↔ t.Finite

Tactic:
rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Retract.lean
lemma le_retracts (P : MorphismProperty C) : P ≤ P.retracts

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.retracts f

Tactic:
exact ⟨_, _, f, { i := 𝟙 _, r := 𝟙 _}, hf⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.retracts

Tactic:
intro X Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.retracts f
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    [hF : Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) :
    (Orientation.map (Fin 2) φ.toLinearEquiv o).kahler x y = o.kahler (φ.symm x) (φ.symm y)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)

Tactic:
simp [kahler_apply_apply, areaForm_map]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_le_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    angle x (x - y) ≤ π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) ≤ π / 2

Tactic:
rw [sub_eq_add_neg]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x + -y) ≤ π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x + -y) ≤ π / 2

Tactic:
exact angle_add_le_pi_div_two_of_inner_eq_zero h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x - y) ≤ π / 2

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) ≤ π / 2
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
private lemma stereographic'_neg {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    stereographic' n (-v) v = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr (↑(stereographic ⋯) v) = 0

Tactic:
simp only [EmbeddingLike.map_eq_zero_iff]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ ↑(stereographic' n (-v)) v = 0

Tactic:
dsimp [stereographic']

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr (↑(stereographic ⋯) v) = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0

Tactic:
apply stereographic_neg_apply

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_encard (h : s ⊆ t) : s.encard ≤ t.encard

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard

Tactic:
exact le_self_add

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
rw [← union_diff_cancel h, encard_union_eq disjoint_sdiff_right]

Result:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernelIsoOfEq_trans {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g)
    (w₂ : g = h) : kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (w₁.trans w₂)

Proof state:
case refl.refl.w.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq ⋯).hom ≫ equalizer.ι f 0 = (kernelIsoOfEq ⋯).hom ≫ equalizer.ι f 0

Tactic:
simp [kernelIsoOfEq]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel h
inst✝ : HasKernel f
w₂ : f = h
⊢ kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

Tactic:
cases w₂

Result:
case refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq ⋯ = kernelIsoOfEq ⋯

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f g h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel g
inst✝ : HasKernel h
w₁ : f = g
w₂ : g = h
⊢ kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

Tactic:
cases w₁

Result:
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel h
inst✝ : HasKernel f
w₂ : f = h
⊢ kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

Proof state:
case refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq ⋯ = kernelIsoOfEq ⋯

Tactic:
ext

Result:
case refl.refl.w.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯ ≪≫ kernelIsoOfEq ⋯).hom ≫ equalizer.ι f 0 = (kernelIsoOfEq ⋯).hom ≫ equalizer.ι f 0
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem equalizerIso_hom_comp_subtype : (equalizerIso g h).hom ≫ Subtype.val = equalizer.ι g h

Proof state:
Y Z : Type u
g h : Y ⟶ Z
⊢ (equalizerIso g h).hom ≫ Subtype.val = equalizer.ι g h

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem div_le_of_le_mul {a b c : ℝ≥0} (h : a ≤ b * c) : a / c ≤ b :=
  if h0 : c = 0 then by simp [h0] else (div_le_iff₀ (pos_iff_ne_zero.2 h0)).2 h

Proof state:
a b c : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

Tactic:
simp [h0]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem X_pow_sub_one_dvd_prod_cyclotomic (R : Type*) [CommRing R] {n m : ℕ} (hpos : 0 < n)
    (hm : m ∣ n) (hdiff : m ≠ n) : X ^ m - 1 ∣ ∏ i ∈ Nat.properDivisors n, cyclotomic i R

Proof state:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1)

Tactic:
exact ⟨∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1) =
    (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hm : m ∣ n
hdiff : m ≠ n
⊢ X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
replace hm := Nat.mem_properDivisors.2
  ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩

Result:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

Proof state:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
rw [← Finset.sdiff_union_of_subset (Nat.divisors_subset_properDivisors (ne_of_lt hpos).symm
  (Nat.mem_properDivisors.1 hm).1 (ne_of_lt (Nat.mem_properDivisors.1 hm).2)),
  Finset.prod_union Finset.sdiff_disjoint,
  prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)]

Result:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1)
-- Mathlib/Probability/Kernel/Disintegration/Basic.lean
lemma IsCondKernel.isProbabilityMeasure [MeasurableSingletonClass α] {a : α} (ha : ρ.fst {a} ≠ 0) :
    IsProbabilityMeasure (ρCond a)

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
a : α
ha : ρ.fst {a} ≠ 0
⊢ IsProbabilityMeasure (ρCond a)

Tactic:
constructor

Result:
case measure_univ
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
a : α
ha : ρ.fst {a} ≠ 0
⊢ (ρCond a) univ = 1

Proof state:
case measure_univ
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
a : α
ha : ρ.fst {a} ≠ 0
⊢ (ρCond a) univ = 1

Tactic:
rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
  (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Icc_add_one_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (a + 1) b = Ioc a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem Perm.kreplace {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) :
    l₁ ~ l₂ → kreplace a b l₁ ~ kreplace a b l₂ :=
  perm_lookmap _ <| by
    refine nd.pairwise_ne.imp ?_
    intro x y h z h₁ w h₂
    split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂
    exact (h (h_2.symm.trans h_1)).elim

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ Pairwise
    (fun a_1 b_1 =>
      ∀ c ∈ if a = a_1.fst then some ⟨a, b⟩ else none,
        ∀ d ∈ if a = b_1.fst then some ⟨a, b⟩ else none, a_1 = b_1 ∧ c = d)
    l₁

Tactic:
refine nd.pairwise_ne.imp ?_

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ c ∈ if a = a_1.fst then some ⟨a, b⟩ else none,
        ∀ d ∈ if a = b_1.fst then some ⟨a, b⟩ else none, a_1 = b_1 ∧ c = d

Proof state:
case pos.refl.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ ⟨a, b⟩ = ⟨a, b⟩

Tactic:
exact (h (h_2.symm.trans h_1)).elim

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ ∀ {a_1 b_1 : Sigma β},
    a_1.fst ≠ b_1.fst →
      ∀ c ∈ if a = a_1.fst then some ⟨a, b⟩ else none,
        ∀ d ∈ if a = b_1.fst then some ⟨a, b⟩ else none, a_1 = b_1 ∧ c = d

Tactic:
intro x y h z h₁ w h₂

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some ⟨a, b⟩ else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some ⟨a, b⟩ else none
⊢ x = y ∧ z = w

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some ⟨a, b⟩ else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some ⟨a, b⟩ else none
⊢ x = y ∧ z = w

Tactic:
split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂

Result:
case pos.refl.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ ⟨a, b⟩ = ⟨a, b⟩
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_mul_le (f g : Perm α) : (f * g).support ≤ f.support ⊔ g.support := fun x => by
  simp only [sup_eq_union]
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  rintro ⟨hf, hg⟩
  rw [hg, hf]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ∪ g.support

Tactic:
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ f x = x ∧ g x = x → f (g x) = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ⊔ g.support

Tactic:
simp only [sup_eq_union]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ∪ g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ f x = x ∧ g x = x → f (g x) = x

Tactic:
rintro ⟨hf, hg⟩

Result:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f (g x) = x

Proof state:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f (g x) = x

Tactic:
rw [hg, hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m

Proof state:
m k : Int
⊢ k * m.tdiv k + m.tmod k = m

Tactic:
apply tdiv_add_tmod

Result:
no goals

Proof state:
m k : Int
⊢ m.tdiv k * k + m.tmod k = m

Tactic:
rw [Int.mul_comm]

Result:
m k : Int
⊢ k * m.tdiv k + m.tmod k = m
-- Mathlib/Data/Finset/NatAntidiagonal.lean
theorem antidiagonal_succ (n : ℕ) :
    antidiagonal (n + 1) =
      cons (0, n + 1)
        ((antidiagonal n).map
          (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Embedding.refl _)))
        (by simp)

Proof state:
n : ℕ
⊢ (0, n + 1) ∉ map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)

Tactic:
simp

Result:
no goals

Proof state:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
        (antidiagonal n).val

Tactic:
apply Multiset.Nat.antidiagonal_succ

Result:
no goals

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯

Tactic:
apply eq_of_veq

Result:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (0, n + 1)
        (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯).val

Proof state:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (0, n + 1)
        (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯).val

Tactic:
rw [cons_val, map_val]

Result:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
        (antidiagonal n).val
-- Mathlib/ModelTheory/Types.lean
theorem exists_modelType_is_realized_in (p : T.CompleteType α) :
    ∃ M : Theory.ModelType.{u, v, max u v w} T, p ∈ T.realizedTypes M α

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
⊢ (T.typeOf fun a => ↑(L.con a)) = p

Tactic:
refine SetLike.ext fun φ => ?_

Result:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ (φ ∈ T.typeOf fun a => ↑(L.con a)) ↔ φ ∈ p

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯)) ⊨ φ ↔ ↑M ⊨ φ

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
⊢ ∃ M, p ∈ T.realizedTypes (↑M) α

Tactic:
obtain ⟨M⟩ := p.isMaximal.1

Result:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
⊢ ∃ M, p ∈ T.realizedTypes (↑M) α

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ (φ ∈ T.typeOf fun a => ↑(L.con a)) ↔ φ ∈ p

Tactic:
simp only [CompleteType.mem_typeOf]

Result:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ((Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ φ ∈ p

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
⊢ ∃ M, p ∈ T.realizedTypes (↑M) α

Tactic:
refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩

Result:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
⊢ (T.typeOf fun a => ↑(L.con a)) = p

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ((Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ φ ∈ p

Tactic:
refine
  (@Formula.realize_equivSentence_symm_con _
    ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
    (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
      (p.isMaximal.mem_iff_models φ).symm)

Result:
case intro
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯)) ⊨ φ ↔ ↑M ⊨ φ
-- 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
⊢ -48 * W.a₄ = 0

Tactic:
linear_combination -24 * W.a₄ * 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
⊢ -48 * W.a₄ = 0
-- Mathlib/Analysis/NormedSpace/BallAction.lean
theorem ne_neg_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0 : E) r) : x ≠ -x := fun h =>
  ne_zero_of_mem_sphere hr x ((self_eq_neg 𝕜 _).mp (by (conv_lhs => rw [h]); rfl))

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑x = -↑x

Tactic:
conv_lhs => rw [h]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑(-x) = -↑x

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑(-x) = -↑x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑x = -↑x

Tactic:
(conv_lhs => rw [h])

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑(-x) = -↑x
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_pow {f : K[X]} (hf : f.Splits i) (n : ℕ) : (f ^ n).Splits i

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits i f
n : ℕ
⊢ Splits i (f ^ n)

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits i f
n : ℕ
⊢ Splits i (∏ _x ∈ Finset.range n, f)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : Splits i f
n : ℕ
⊢ Splits i (∏ _x ∈ Finset.range n, f)

Tactic:
exact splits_prod i fun j _ => hf

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem coeff_truncate {m : ℕ} (hm : n ≤ m) (i : Fin n) (x : TruncatedWittVector p m R) :
    (truncate hm x).coeff i = x.coeff (Fin.castLE hm i)

Proof state:
case intro
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
y : 𝕎 R
⊢ coeff i ((truncate hm) ((WittVector.truncate m) y)) = coeff (Fin.castLE hm i) ((WittVector.truncate m) y)

Tactic:
simp only [truncate_wittVector_truncate, WittVector.coeff_truncate, Fin.coe_castLE]

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
x : TruncatedWittVector p m R
⊢ coeff i ((truncate hm) x) = coeff (Fin.castLE hm i) x

Tactic:
obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x

Result:
case intro
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
y : 𝕎 R
⊢ coeff i ((truncate hm) ((WittVector.truncate m) y)) = coeff (Fin.castLE hm i) ((WittVector.truncate m) y)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem Measurable.nnreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0} (h : ∀ i, Measurable (f i)) :
    Measurable fun x => ∑' i, f i x

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ∑' (i : ι), f i x

Tactic:
simp_rw [NNReal.tsum_eq_toNNReal_tsum]

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => (∑' (b : ι), ↑(f b x)).toNNReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => (∑' (b : ι), ↑(f b x)).toNNReal

Tactic:
exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma arg_eq_zero_iff_zero_le {z : ℂ} : arg z = 0 ↔ 0 ≤ z

Proof state:
z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z

Tactic:
rw [arg_eq_zero_iff, eq_comm, nonneg_iff]

Result:
no goals