harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule R M) :
    Module.rank R (s ⊔ t : Submodule R M) ≤ Module.rank R s + Module.rank R t

Proof state:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t

Tactic:
rw [← Submodule.rank_sup_add_rank_inf_eq]

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t)

Proof state:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t)

Tactic:
exact self_le_add_right _ _

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_prod_prod_le_of_le (s : Finset ι) {f a : ι → E} {d : ι → ℝ}
    (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) :
    dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, dist (f b) (a b) ≤ d b
⊢ dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Tactic:
simp only [dist_eq_norm_div, ← Finset.prod_div_distrib] at *

Result:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖f b / a b‖ ≤ d b
⊢ ‖∏ x ∈ s, f x / a x‖ ≤ ∑ b ∈ s, d b

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖f b / a b‖ ≤ d b
⊢ ‖∏ x ∈ s, f x / a x‖ ≤ ∑ b ∈ s, d b

Tactic:
exact norm_prod_le_of_le s h

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isSkewAdjoint_iff_neg_self_adjoint (f : M → M) :
    B.IsSkewAdjoint f ↔ IsAdjointPair (-B) B f f :=
  show (∀ x y, B (f x) y = B x ((-f) y)) ↔ ∀ x y, B (f x) y = (-B) x (f y) by simp

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : M → M
⊢ (∀ (x y : M), (B (f x)) y = (B x) ((-f) y)) ↔ ∀ (x y : M), (B (f x)) y = ((-B) x) (f y)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma surjectiveOnStalks_of_surjective (h : Function.Surjective f) :
    SurjectiveOnStalks f :=
  surjectiveOnStalks_iff_forall_ideal.mpr fun _ _ s ↦
    let ⟨r, hr⟩ := h s
    ⟨r, 1, 1, by simpa [← Ideal.eq_top_iff_one], by simpa [← Ideal.eq_top_iff_one], by simp [hr]⟩

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ f 1 ∉ x✝¹

Tactic:
simpa [← Ideal.eq_top_iff_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ 1 ∉ x✝¹

Tactic:
simpa [← Ideal.eq_top_iff_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ 1 * f 1 * s = 1 * f r

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem ConvexOn.secant_mono_aux2 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
    (hxy : x < y) (hyz : y < z) : (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Tactic:
rw [div_le_div_iff₀ hxy' hxz']

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) ≤ (f z - f x) * (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Tactic:
have hxz' : 0 < z - x := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Tactic:
have hxy' : 0 < y - x := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) ≤ (f z - f x) * (y - x)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - x

Tactic:
linarith

Result:
no goals
-- Mathlib/NumberTheory/FrobeniusNumber.lean
theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
    FrobeniusNumber (m * n - m - n) {m, n}

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : k ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
⊢ k ≤ m * n - m - n

Tactic:
dsimp at hk

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : ¬∃ m_1 n_1, m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n = ↑m * ↑n

Tactic:
rw [← sub_eq_zero] at h ⊢

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0

Proof state:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ a * m + b * n = k

Tactic:
rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]

Result:
no goals

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m

Tactic:
exact
  ModEq.le_of_lt_add
    (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub' (dvd_mul_right m n) dvd_rfl)).symm)
    (lt_of_lt_of_le hx le_tsub_add)

Result:
no goals

Proof state:
case intro.intro
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩

Result:
no goals

Proof state:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)

Tactic:
have hmn : m + n ≤ m * n := add_le_mul hm hn

Result:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ upperBounds {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}

Tactic:
intro k hk

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : k ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
⊢ k ≤ m * n - m - n
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mulEquivOfLocalizations_right_inv_apply {k : LocalizationMap S P} {x} :
    (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
k : S.LocalizationMap P
x : M
⊢ (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : X.δ i.succ ≫ X.σ i = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_succ, X.map_id]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_monic : Monic (minpolyDiv R x)

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff = 1
⊢ (minpolyDiv R x).Monic

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ (minpolyDiv R x).Monic

Tactic:
have := congr_arg leadingCoeff (minpolyDiv_spec R x)

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).Monic

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
⊢ (minpolyDiv R x).Monic

Tactic:
nontriviality S

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ (minpolyDiv R x).Monic

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0

Tactic:
simpa using minpolyDiv_ne_zero hx

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).Monic

Tactic:
rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff = 1
⊢ (minpolyDiv R x).Monic

R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
this : (minpolyDiv R x * (X - C x)).leadingCoeff = (map (algebraMap R S) (minpoly R x)).leadingCoeff
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma densityProcess_mono_kernel_left {κ' : Kernel α (γ × β)} (hκκ' : κ ≤ κ')
    (hκ'ν : fst κ' ≤ ν) (n : ℕ) (a : α) (x : γ) (s : Set β) :
    densityProcess κ ν n a x s ≤ densityProcess κ' ν n a x s

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤
    ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal

Tactic:
gcongr

Result:
case neg.hb
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ (κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ⊤

case neg.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ' a) (countablePartitionSet n x ×ˢ s)
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem any_eq (p : α → β → Bool) (l : AssocList α β) :
    any p l = l.toList.any fun (a, b) => p a b

Proof state:
α : Type u_1
β : Type u_2
p : α → β → Bool
l : AssocList α β
⊢ any p l =
    l.toList.any fun x =>
      match x with
      | (a, b) => p a b

Tactic:
induction l <;> simp [any, *]

Result:
no goals
-- Mathlib/Algebra/Star/Unitary.lean
theorem _root_.IsUnit.mem_unitary_of_star_mul_self  {u : R} (hu : IsUnit u)
    (h_mul : star u * u = 1) : u ∈ unitary R

Proof state:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u * star u = 1

Tactic:
lift u to Rˣ using hu

Result:
case intro
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : Rˣ
h_mul : star ↑u * ↑u = 1
⊢ ↑u * star ↑u = 1

Proof state:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u ∈ unitary R

Tactic:
refine unitary.mem_iff.mpr ⟨h_mul, ?_⟩

Result:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u * star u = 1

Proof state:
case intro
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : Rˣ
h_mul : star ↑u * ↑u = 1
⊢ ↑u * star ↑u = 1

Tactic:
exact left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem add_le_nadd : a + b ≤ a ♯ b

Proof state:
case H₃
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c

Tactic:
rw [(isNormal_add_right a).apply_of_isLimit hc, Ordinal.iSup_le_iff]

Result:
case H₃
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a + o' ≤ a ♯ o'
⊢ ∀ (i : ↑(Iio c)), a + ↑i ≤ a ♯ c

Proof state:
case H₃.mk
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a + o' ≤ a ♯ o'
i : Ordinal.{u}
hi : i ∈ Iio c
⊢ a + ↑⟨i, hi⟩ ≤ a ♯ c

Tactic:
exact (H i hi).trans (nadd_le_nadd_left hi.le a)

Result:
no goals

Proof state:
case H₁
a b : Ordinal.{u}
⊢ a + 0 ≤ a ♯ 0

Tactic:
simp

Result:
no goals

Proof state:
case H₃
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a + o' ≤ a ♯ o'
⊢ ∀ (i : ↑(Iio c)), a + ↑i ≤ a ♯ c

Tactic:
rintro ⟨i, hi⟩

Result:
case H₃.mk
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a + o' ≤ a ♯ o'
i : Ordinal.{u}
hi : i ∈ Iio c
⊢ a + ↑⟨i, hi⟩ ≤ a ♯ c

Proof state:
a b : Ordinal.{u}
⊢ a + b ≤ a ♯ b

Tactic:
induction b using limitRecOn with
| H₁ => simp
| H₂ c h =>
  rwa [add_succ, nadd_succ, succ_le_succ_iff]
| H₃ c hc H =>
  rw [(isNormal_add_right a).apply_of_isLimit hc, Ordinal.iSup_le_iff]
  rintro ⟨i, hi⟩
  exact (H i hi).trans (nadd_le_nadd_left hi.le a)

Result:
no goals

Proof state:
case H₂
a b c : Ordinal.{u}
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c

Tactic:
rwa [add_succ, nadd_succ, succ_le_succ_iff]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp, norm_cast]
lemma nnnorm_real (r : ℝ) : ‖(r : ℂ)‖₊ = ‖r‖₊

Proof state:
case a
r : ℝ
⊢ ↑‖↑r‖₊ = ↑‖r‖₊

Tactic:
exact norm_real _

Result:
no goals

Proof state:
r : ℝ
⊢ ‖↑r‖₊ = ‖r‖₊

Tactic:
ext

Result:
case a
r : ℝ
⊢ ↑‖↑r‖₊ = ↑‖r‖₊
-- Mathlib/Data/Finmap.lean
theorem union_empty {s₁ : Finmap β} : s₁ ∪ ∅ = s₁ :=
  induction_on s₁ fun s₁ => by
    rw [← empty_toFinmap]
    simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ∅ = ⟦s₁⟧

Tactic:
rw [← empty_toFinmap]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧

Tactic:
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_eq_bot_of_injective (inj : Function.Injective f) (h : jacobson R₂ M₂ = ⊥) :
    jacobson R M = ⊥ :=
  le_bot_iff.mp <| (le_comap_jacobson f).trans <| by
    simp_rw [h, comap_bot, ((LinearMapClass.ker_eq_bot _).mpr inj).le]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
inj : Function.Injective ⇑f
h : jacobson R₂ M₂ = ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥

Tactic:
simp_rw [h, comap_bot, ((LinearMapClass.ker_eq_bot _).mpr inj).le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem get_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {a : α} {h : a ∈ m} :
    m.get a h = Raw₀.get ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
      (by change dite .. = true at h; split at h <;> simp_all) := rfl

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : a ∈ m
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
change dite .. = true at h

Result:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : a ∈ m
⊢ 0 < m.buckets.size

Tactic:
change dite .. = true at h

Result:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
split at h <;> simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem det_rotation (θ : Real.Angle) : LinearMap.det (o.rotation θ).toLinearMap = 1

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Tactic:
haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Proof state:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Tactic:
rw [o.rotation_eq_matrix_toLin θ hx]

Result:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det
      ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx))
        !![θ.cos, -θ.sin; θ.sin, θ.cos]) =
    1

Proof state:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det
      ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx))
        !![θ.cos, -θ.sin; θ.sin, θ.cos]) =
    1

Tactic:
simpa [sq] using θ.cos_sq_add_sin_sq

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Result:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1