harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem le_smul_caratheodory (a : ℝ≥0∞) (m : OuterMeasure α) :
    m.caratheodory ≤ (a • m).caratheodory := fun s h t => by
      simp only [smul_apply, smul_eq_mul]
      rw [(isCaratheodory_iff m).mp h t]
      simp [mul_add]

Proof state:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ (a • m) t = (a • m) (t ∩ s) + (a • m) (t \ s)

Tactic:
simp only [smul_apply, smul_eq_mul]

Result:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * m t = a * m (t ∩ s) + a * m (t \ s)

Proof state:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (m (t ∩ s) + m (t \ s)) = a * m (t ∩ s) + a * m (t \ s)

Tactic:
simp [mul_add]

Result:
no goals

Proof state:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * m t = a * m (t ∩ s) + a * m (t \ s)

Tactic:
rw [(isCaratheodory_iff m).mp h t]

Result:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (m (t ∩ s) + m (t \ s)) = a * m (t ∩ s) + a * m (t \ s)
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b c : α
⊢ a / b ⊔ a / c = a / (b ⊓ c)

Tactic:
simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk0_eq_mk0_inv_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} :
    ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔
      ∃ x ≠ (0 : R), I * J = Ideal.span {x}

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = Submodule.span R {a}
⊢ a ≠ 0

Tactic:
by_contra!

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = Submodule.span R {a}
this : a = 0
⊢ False

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = ⊥
this : a = 0
⊢ False

Tactic:
exact nonZeroDivisors.coe_ne_zero _ <| J.prop _ ha

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ a, ↑I * ↑J = Submodule.span R {a}) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = Submodule.span R {a}
⊢ a ≠ 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ mk0 I = (mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Tactic:
rw [eq_inv_iff_mul_eq_one, ← _root_.map_mul, ClassGroup.mk0_eq_one_iff,
  Submodule.isPrincipal_iff, Submonoid.coe_mul]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ a, ↑I * ↑J = Submodule.span R {a}) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = Submodule.span R {a}
this : a = 0
⊢ False

Tactic:
rw [this, Submodule.span_zero_singleton] at ha

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}
a : R
ha : ↑I * ↑J = ⊥
this : a = 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    (m.erase k).size = if k ∈ m then m.size - 1 else m.size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).size = if m.contains k = true then m.size - 1 else m.size

Tactic:
simp_to_raw using Raw₀.size_erase

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).size = if k ∈ m then m.size - 1 else m.size

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).size = if m.contains k = true then m.size - 1 else m.size
-- Mathlib/Algebra/Lie/Abelian.lean
theorem LieSubmodule.trivial_lie_oper_zero [LieModule.IsTrivial L M] : ⁅I, N⁆ = ⊥

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥

Tactic:
rw [trivial_lie_zero] at h

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ ↑⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Tactic:
rintro m ⟨x, n, h⟩

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ ↑⊥

Tactic:
simp [← h]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ = ⊥

Tactic:
suffices ⁅I, N⁆ ≤ ⊥ from le_bot_iff.mp this

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.fromBlocks_of_isSymm [Zero α] {A : Matrix m m α} {C : Matrix n m α}
    {D : Matrix n n α} (h : (A.fromBlocks 0 C D).IsSymm) (ha : A.IsDiag) (hd : D.IsDiag) :
    (A.fromBlocks 0 C D).IsDiag

Proof state:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0ᵀ D).IsDiag

Tactic:
exact ha.fromBlocks hd

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 C D).IsDiag

Tactic:
rw [← (isSymm_fromBlocks_iff.1 h).2.1]

Result:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0ᵀ D).IsDiag
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) :
    repr a + m < ω ^ repr e

Proof state:
case intro.intro
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
apply principal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (nat_lt_omega0 _) _)

Result:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr

Proof state:
case intro
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)

Result:
case intro.intro
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ a.repr + ↑m < ω ^ e.repr

Proof state:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
obtain ⟨h₁, h₂⟩ := nf_repr_split h

Result:
case intro
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
⊢ a.repr + ↑m < ω ^ e.repr

Proof state:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr

Tactic:
simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)

Result:
no goals
-- Mathlib/Topology/Clopen.lean
theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b)
    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (s ∩ a)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClopen (s ∩ a)

Tactic:
refine ⟨?_, IsOpen.inter h.2 ha⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClosed (s ∩ a)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ a

Tactic:
simpa [not_mem_of_mem_compl hx₂] using cover hx₁

Result:
no goals

Proof state:
case h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ

Tactic:
refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_

Result:
case h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ s ∩ bᶜ ⊆ s ∩ a

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ IsClosed (s ∩ a)

Tactic:
convert this using 1

Result:
case h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ

Proof state:
case h.e'_3.intro
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ s ∩ a

Tactic:
exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClosed (s ∩ a)

Tactic:
have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)

Result:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ IsClosed (s ∩ a)

Proof state:
case h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
⊢ s ∩ bᶜ ⊆ s ∩ a

Tactic:
rintro x ⟨hx₁, hx₂⟩

Result:
case h.e'_3.intro
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ s ∩ a
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.sin (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
  sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem adj_getVert_succ {u v} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) :
    G.Adj (w.getVert i) (w.getVert (i + 1))

Proof state:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Tactic:
exact ih (Nat.succ_lt_succ_iff.1 hi)

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
i : ℕ
hi : i < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert i) ((cons hxy p✝).getVert (i + 1))

Tactic:
cases i

Result:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
hi : 0 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert 0) ((cons hxy p✝).getVert (0 + 1))

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Proof state:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
hi : 0 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert 0) ((cons hxy p✝).getVert (0 + 1))

Tactic:
simp [getVert, hxy]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : i < nil.length
⊢ G.Adj (nil.getVert i) (nil.getVert (i + 1))

Tactic:
cases hi

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma rTensor.inverse_of_rightInverse_apply
    {h : P → N} (hgh : Function.RightInverse h g) (y : N ⊗[R] Q) :
    (rTensor.inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y) =
      Submodule.Quotient.mk (p := LinearMap.range (rTensor Q f)) y

Proof state:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q)

Tactic:
rw [Submodule.Quotient.eq, ← TensorProduct.sub_tmul]

Result:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ (h (g n) - n) ⊗ₜ[R] q ∈ range (rTensor Q f)

Proof state:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (n ⊗ₜ[R] q) = (range (rTensor Q f)).mkQ (n ⊗ₜ[R] q)

Tactic:
simp? [rTensor.inverse_of_rightInverse] says
  simp only [inverse_of_rightInverse, coe_comp, Function.comp_apply, rTensor_tmul,
    lift.tmul, coe_mk, AddHom.coe_mk, mk_apply, Submodule.mkQ_apply]

Result:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q)
-- Mathlib/Algebra/Field/Periodic.lean
theorem Periodic.const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  by_cases ha : a = 0
  · simp only [ha, zero_smul]
  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

Tactic:
simp only [ha, zero_smul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

Tactic:
by_cases ha : a = 0

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_div_le_mul_div_assoc (a b c : ℕ) : a * (b / c) ≤ a * b / c :=
  if hc0 : c = 0 then by simp [hc0] else
    (Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero hc0)).2
      (by rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _))

Proof state:
a b c : ℕ
hc0 : c = 0
⊢ a * (b / c) ≤ a * b / c

Tactic:
simp [hc0]

Result:
no goals

Proof state:
a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c) * c ≤ a * b

Tactic:
rw [Nat.mul_assoc]

Result:
a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c * c) ≤ a * b

Proof state:
a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c * c) ≤ a * b

Tactic:
exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem hermite_one : hermite 1 = X

Proof state:
⊢ hermite 1 = X

Tactic:
rw [hermite_succ, hermite_zero]

Result:
⊢ X * C 1 - derivative (C 1) = X

Proof state:
⊢ X * C 1 - derivative (C 1) = X

Tactic:
simp only [map_one, mul_one, derivative_one, sub_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Cardinality.lean
theorem continuum_le_cardinal_of_module
    (𝕜 : Type u) (E : Type v) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] : 𝔠 ≤ #E

Proof state:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜

Tactic:
simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜

Result:
no goals

Proof state:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ 𝔠 ≤ #E

Tactic:
have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
  simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜

Result:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
⊢ 𝔠 ≤ #E

Proof state:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
⊢ 𝔠 ≤ #E

Tactic:
simpa using A.trans (Cardinal.mk_le_of_module 𝕜 E)

Result:
no goals