harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_def (a b : Ordinal) :
    a ⨳ b = sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}

Proof state:
a b : Ordinal.{u_1}
⊢ a ⨳ b = sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}

Tactic:
rw [nmul]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma toCycles_comp_homologyπ [K.HasHomology j] :
    K.toCycles i j ≫ K.homologyπ j = 0 :=
  K.liftCycles_homologyπ_eq_zero_of_boundary (K.d i j) (c.next j) rfl (𝟙 _) (by simp)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
⊢ K.d i j = 𝟙 (K.X i) ≫ K.d i j

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ)

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
⊢ Injective ((fun x1 x2 => x1 • x2) ∘ ⇑of)

Tactic:
intros _ _ h

Result:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁✝ a₂✝ : G
h : ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁✝ a₂✝ : G
h : ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₂✝
w : NormalWord d
⊢ a₁✝ • w = a₂✝ • w

Tactic:
simp_all [funext_iff, of_smul_eq_smul]

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁✝ a₂✝ : G
h : ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑of) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
  by simp_all [funext_iff, of_smul_eq_smul])

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
⊢ Injective ⇑of

Tactic:
rcases TransversalPair.nonempty G A B with ⟨d⟩

Result:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
⊢ Injective ⇑of
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_ncard_of_injOn {t : Set β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : InjOn f s)
    (ht : t.Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : autoParam t.Finite _auto✝
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard

Tactic:
rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : autoParam t.Finite _auto✝
hle : s.encard ≤ t.encard
⊢ s.ncard ≤ t.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : autoParam t.Finite _auto✝
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : autoParam t.Finite _auto✝
⊢ s.ncard ≤ t.ncard

Tactic:
have hle := encard_le_encard_of_injOn hf f_inj

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : autoParam t.Finite _auto✝
hle : s.encard ≤ t.encard
⊢ s.ncard ≤ t.ncard
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma toSheafify_pullbackSheafificationCompatibility (F : Dᵒᵖ ⥤ A) :
    toSheafify J (G.op ⋙ F) ≫
    ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft _ (toSheafify K _)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)

Tactic:
let adj₁ := G.op.ranAdjunction A

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem edist_le_of_edist_le_geometric_two_of_tendsto (n : ℕ) : edist (f n) a ≤ 2 * C / 2 ^ n

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2

Tactic:
convert edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n

Tactic:
rw [mul_assoc, mul_comm]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)

Tactic:
rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ 2 * C / 2 ^ n

Tactic:
simp only [div_eq_mul_inv, ENNReal.inv_pow] at *

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
ha : o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ o.oangle x y = 0

Tactic:
rw [h] at ha

Result:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
ha : o.oangle x y = ↑0 ∨ o.oangle x y = -↑0
⊢ o.oangle x y = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0

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

Result:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x y = 0
⊢ InnerProductGeometry.angle x y = 0

case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
⊢ o.oangle x y = 0

Proof state:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x y = 0
⊢ InnerProductGeometry.angle x y = 0

Tactic:
simpa [o.angle_eq_abs_oangle_toReal hx hy]

Result:
no goals

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
⊢ o.oangle x y = 0

Tactic:
have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy

Result:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
ha : o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ o.oangle x y = 0

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
ha : o.oangle x y = ↑0 ∨ o.oangle x y = -↑0
⊢ o.oangle x y = 0

Tactic:
simpa using ha

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
@[simp]
lemma inv_add_add_mul_eq_zero (u : (PreQuasiregular R)ˣ) :
    u⁻¹.val.val + u.val.val + u.val.val * u⁻¹.val.val = 0

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0

Tactic:
simpa [-Units.mul_inv] using congr($(u.mul_inv).val)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem zero_mk (s : S) : mk (0 : M) s = 0 :=
  mk_eq.mpr ⟨1, by rw [one_smul, smul_zero, smul_zero, one_smul]⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
⊢ 1 • 1 • 0 = 1 • s • 0

Tactic:
rw [one_smul, smul_zero, smul_zero, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_setWidth (i : Nat) (x : BitVec n) :
    BitVec.toNat (setWidth i x) = x.toNat % 2^i

Proof state:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (setWidth i { toFin := ⟨x, lt_n⟩ }).toNat = { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Tactic:
simp only [setWidth]

Result:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Proof state:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
n_le_i : n ≤ i
x_lt_two_i : x < 2 ^ i
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Tactic:
simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]

Result:
no goals

Proof state:
n i : Nat
x : BitVec n
⊢ (setWidth i x).toNat = x.toNat % 2 ^ i

Tactic:
let ⟨x, lt_n⟩ := x

Result:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (setWidth i { toFin := ⟨x, lt_n⟩ }).toNat = { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Proof state:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
n_le_i : ¬n ≤ i
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Tactic:
simp [n_le_i, toNat_ofNat]

Result:
no goals

Proof state:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
n_le_i : n ≤ i
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Tactic:
have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i

Result:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
n_le_i : n ≤ i
x_lt_two_i : x < 2 ^ i
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Proof state:
n i : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (if h : n ≤ i then setWidth' h { toFin := ⟨x, lt_n⟩ } else BitVec.ofNat i { toFin := ⟨x, lt_n⟩ }.toNat).toNat =
    { toFin := ⟨x, lt_n⟩ }.toNat % 2 ^ i

Tactic:
if n_le_i : n ≤ i then
  have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i
  simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]
else
  simp [n_le_i, toNat_ofNat]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_add_right (μ : Measure α) (κ η : Kernel α β)
    [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
by_cases hμ : SFinite μ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
simp [hμ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
    (Const.alter m k f).contains k' =
      if k == k' then
        (f (Const.get? m k)).isSome
      else
        m.contains k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : Option β → Option β
⊢ (alter m k f).contains k' = if (k == k') = true then (f (get? m k)).isSome else m.contains k'

Tactic:
simp_to_model [Const.alter] using List.Const.containsKey_alterKey

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Defs.lean
theorem subsingleton_iff : Subsingleton (Submonoid M) ↔ Subsingleton M :=
  ⟨fun _ =>
    ⟨fun x y =>
      have : ∀ i : M, i = 1 := fun i =>
        mem_bot.mp <| Subsingleton.elim (⊤ : Submonoid M) ⊥ ▸ mem_top i
      (this x).trans (this y).symm⟩,
    fun _ =>
    ⟨fun x y => Submonoid.ext fun i => Subsingleton.elim 1 i ▸ by simp [Submonoid.one_mem]⟩⟩

Proof state:
M : Type u_1
inst✝ : MulOneClass M
x✝ : Subsingleton M
x y : Submonoid M
i : M
⊢ 1 ∈ x ↔ 1 ∈ y

Tactic:
simp [Submonoid.one_mem]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem intCast_complex_norm (x : ℤ[i]) : (x.norm : ℂ) = Complex.normSq (x : ℂ)

Proof state:
x : ℤ[i]
⊢ ↑(norm x) = ↑(normSq (toComplex x))

Tactic:
cases x

Result:
case mk
re✝ im✝ : ℤ
⊢ ↑{ re := re✝, im := im✝ }.norm = ↑(normSq (toComplex { re := re✝, im := im✝ }))

Proof state:
case mk
re✝ im✝ : ℤ
⊢ ↑{ re := re✝, im := im✝ }.norm = ↑(normSq (toComplex { re := re✝, im := im✝ }))

Tactic:
rw [Zsqrtd.norm, normSq]

Result:
case mk
re✝ im✝ : ℤ
⊢ ↑({ re := re✝, im := im✝ }.re * { re := re✝, im := im✝ }.re -
        -1 * { re := re✝, im := im✝ }.im * { re := re✝, im := im✝ }.im) =
    ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
          map_mul' := normSq.proof_3 }
        (toComplex { re := re✝, im := im✝ }))

Proof state:
case mk
re✝ im✝ : ℤ
⊢ ↑({ re := re✝, im := im✝ }.re * { re := re✝, im := im✝ }.re -
        -1 * { re := re✝, im := im✝ }.im * { re := re✝, im := im✝ }.im) =
    ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
          map_mul' := normSq.proof_3 }
        (toComplex { re := re✝, im := im✝ }))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NatAntidiagonal.lean
@[simp] lemma antidiagonal_filter_le_fst_of_le {n k : ℕ} (h : k ≤ n) :
    (antidiagonal n).filter (fun a ↦ k ≤ a.fst) = (antidiagonal (n - k)).map
      (Embedding.prodMap ⟨_, add_left_injective k⟩ (Embedding.refl ℕ))

Proof state:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => k ≤ a.1) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa

Result:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i

Proof state:
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
⊢ (i, j) ∈ filter (fun a => k ≤ a.1) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
simpa

Result:
no goals

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k

Tactic:
refine ⟨?_, Nat.le_add_left k l⟩

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n

Proof state:
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.1) (antidiagonal n) =
    map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
ext ⟨i, j⟩

Result:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => k ≤ a.1) (antidiagonal n) ↔
    (i, j) ∈ map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Proof state:
case h.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i

Tactic:
refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩

Result:
case h.mk.refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i - k + j = n - k

case h.mk.refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i

Proof state:
case h.mk.refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i

Tactic:
rintro ⟨l, hl, rfl⟩

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k

Proof state:
case h.mk.refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i - k + j = n - k

Tactic:
rw [← Nat.sub_add_comm hi.2, hi.1]

Result:
no goals

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n

Tactic:
exact tsub_add_cancel_of_le h

Result:
no goals

Proof state:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n

Tactic:
rw [add_right_comm, hl]

Result:
case h.mk.refine_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem pow_end {f : Function.End α} (h : LocallyLipschitz f) :
    ∀ n : ℕ, LocallyLipschitz (f ^ n : Function.End α)
  | 0 => by simpa only [pow_zero] using LocallyLipschitz.id
  | n + 1 => by
    rw [pow_succ]
    exact (h.pow_end n).mul_end h

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
⊢ LocallyLipschitz (f ^ 0)

Tactic:
simpa only [pow_zero] using LocallyLipschitz.id

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ n * f)

Tactic:
exact (h.pow_end n).mul_end h

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ (n + 1))

Tactic:
rw [pow_succ]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ n * f)
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem homothety_add (c : P1) (r₁ r₂ : k) :
    homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
r₁ r₂ : k
⊢ homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂

Tactic:
simp only [homothety_def, add_smul, vadd_vadd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_measure (f : α → ℝ≥0∞) (μ ν : Measure α) :
    ∫⁻ a, f a ∂(μ + ν) = ∫⁻ a, f a ∂μ + ∫⁻ a, f a ∂ν

Proof state:
case mk.mk
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ (↑⟨φ, hφ⟩).lintegral μ + (↑⟨ψ, hψ⟩).lintegral ν ≤ (↑⟨φ ⊔ ψ, ⋯⟩).lintegral μ + (↑⟨φ ⊔ ψ, ⋯⟩).lintegral ν

Tactic:
apply_rules [add_le_add, SimpleFunc.lintegral_mono, le_rfl]

Result:
case mk.mk.h₁.hfg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ↑⟨φ, hφ⟩ ≤ ↑⟨φ ⊔ ψ, ⋯⟩

case mk.mk.h₂.hfg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ↑⟨ψ, hψ⟩ ≤ ↑⟨φ ⊔ ψ, ⋯⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ∀ (i j : { i // ⇑i ≤ fun a => f a }), ∃ k, (↑i).lintegral μ + (↑j).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν

Tactic:
rintro ⟨φ, hφ⟩ ⟨ψ, hψ⟩

Result:
case mk.mk
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ∃ k, (↑⟨φ, hφ⟩).lintegral μ + (↑⟨ψ, hψ⟩).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ⨆ x, (↑x).lintegral μ + (↑x).lintegral ν = (⨆ x, (↑x).lintegral μ) + ⨆ x, (↑x).lintegral ν

Tactic:
refine (ENNReal.iSup_add_iSup ?_).symm

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ∀ (i j : { i // ⇑i ≤ fun a => f a }), ∃ k, (↑i).lintegral μ + (↑j).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν

Tactic:
simp only [lintegral, SimpleFunc.lintegral_add, iSup_subtype']

Result:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ⨆ x, (↑x).lintegral μ + (↑x).lintegral ν = (⨆ x, (↑x).lintegral μ) + ⨆ x, (↑x).lintegral ν

Proof state:
case mk.mk.h₁.hfg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ↑⟨φ, hφ⟩ ≤ ↑⟨φ ⊔ ψ, ⋯⟩

case mk.mk.h₂.hfg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ↑⟨ψ, hψ⟩ ≤ ↑⟨φ ⊔ ψ, ⋯⟩

Tactic:
exacts [le_sup_left, le_sup_right]

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ ∃ k, (↑⟨φ, hφ⟩).lintegral μ + (↑⟨ψ, hψ⟩).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν

Tactic:
refine ⟨⟨φ ⊔ ψ, sup_le hφ hψ⟩, ?_⟩

Result:
case mk.mk
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a => f a
⊢ (↑⟨φ, hφ⟩).lintegral μ + (↑⟨ψ, hψ⟩).lintegral ν ≤ (↑⟨φ ⊔ ψ, ⋯⟩).lintegral μ + (↑⟨φ ⊔ ψ, ⋯⟩).lintegral ν