harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ENNReal/Inv.lean
lemma iSup_add_iSup (h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i

Proof state:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Proof state:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Result:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i

Proof state:
case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
simp only [iSup_of_empty, bot_eq_zero, zero_add]

Result:
no goals

Proof state:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i

Tactic:
refine iSup_add_iSup_le fun i j => ?_

Result:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i

Proof state:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
rcases h i j with ⟨k, hk⟩

Result:
case inr.intro
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Proof state:
case inr.intro
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
exact le_iSup_of_le k hk

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
lemma pos_iff [Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K} : 0 < v x ↔ x ≠ 0

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
⊢ 0 < v x ↔ x ≠ 0

Tactic:
rw [zero_lt_iff, ne_zero_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_neg (f : α → E) (m : MeasurableSpace α) : μ[-f|m] =ᵐ[μ] -μ[f|m]

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
m : MeasurableSpace α
⊢ μ[-f|m] =ᶠ[ae μ] -μ[f|m]

Tactic:
calc
  μ[-f|m] = μ[(-1 : ℝ) • f|m] := by rw [neg_one_smul ℝ f]
  _ =ᵐ[μ] (-1 : ℝ) • μ[f|m] := condExp_smul ..
  _ = -μ[f|m] := neg_one_smul ℝ (μ[f|m])

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
m : MeasurableSpace α
⊢ μ[-f|m] = μ[-1 • f|m]

Tactic:
rw [neg_one_smul ℝ f]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Lucas.lean
theorem choose_modEq_prod_range_choose_nat {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
    choose n k ≡ ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [MOD p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ n.choose k ≡ ∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
exact_mod_cast choose_modEq_prod_range_choose ha₁ ha₂

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem IsPreirreducible.image (H : IsPreirreducible s) (f : X → Y) (hf : ContinuousOn f s) :
    IsPreirreducible (f '' s)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ v

Tactic:
rw [← mem_preimage]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' v

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ s
hxu : f x ∈ u
y : X
hy : y ∈ s
hyv : f y ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rw [← mem_preimage] at hxu hyv

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen u
hv : IsOpen v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ (f '' s ∩ (u ∩ v)).Nonempty
-- Mathlib/Algebra/Group/Commute/Units.lean
lemma isUnit_pow_iff_of_not_isUnit (hx : ¬ IsUnit a) {n : ℕ} :
    IsUnit (a ^ n) ↔ n = 0

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ n) ↔ n = 0

Tactic:
rcases n with (_|n) <;>
simp [hx]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem add_ne_zero_of_lt {a b : Nimber} (h : b < a) : a + b ≠ 0

Proof state:
a b : Nimber
h : b < a
⊢ a + b ≠ 0

Tactic:
rw [add_ne_zero_iff]

Result:
a b : Nimber
h : b < a
⊢ a ≠ b

Proof state:
a b : Nimber
h : b < a
⊢ a ≠ b

Tactic:
exact h.ne'

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem toComplex_comp_ofComplex : toComplex.comp ofComplex = AlgHom.id ℝ ℂ

Proof state:
⊢ toComplex.comp ofComplex = AlgHom.id ℝ ℂ

Tactic:
ext1

Result:
case h

⊢ (toComplex.comp ofComplex) Complex.I = (AlgHom.id ℝ ℂ) Complex.I

Proof state:
case h

⊢ (toComplex.comp ofComplex) Complex.I = (AlgHom.id ℝ ℂ) Complex.I

Tactic:
dsimp only [AlgHom.comp_apply, Subtype.coe_mk, AlgHom.id_apply]

Result:
case h

⊢ toComplex (ofComplex Complex.I) = Complex.I

Proof state:
case h

⊢ toComplex (ofComplex Complex.I) = Complex.I

Tactic:
rw [ofComplex_I, toComplex_ι, one_smul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_of_le_two (ho : o ≤ 2) : Principal (· * ·) o

Proof state:
case inl.inl
o : Ordinal.{u}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
ho : o < 1
⊢ Principal (fun x1 x2 => x1 * x2) 0

Tactic:
exact principal_zero

Result:
no goals

Proof state:
case inr
ho : 2 ≤ 2
⊢ Principal (fun x1 x2 => x1 * x2) 2

Tactic:
exact principal_mul_two

Result:
no goals

Proof state:
case inl
o : Ordinal.{u}
ho✝ : o ≤ 2
ho : o < 2
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
rw [← succ_one, lt_succ_iff] at ho

Result:
case inl
o : Ordinal.{u}
ho✝ : o ≤ 2
ho : o ≤ 1
⊢ Principal (fun x1 x2 => x1 * x2) o

Proof state:
case inl.inr
ho✝ : 1 ≤ 2
ho : 1 ≤ 1
⊢ Principal (fun x1 x2 => x1 * x2) 1

Tactic:
exact principal_mul_one

Result:
no goals

Proof state:
o : Ordinal.{u}
ho : o ≤ 2
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
rcases lt_or_eq_of_le ho with (ho | rfl)

Result:
case inl
o : Ordinal.{u}
ho✝ : o ≤ 2
ho : o < 2
⊢ Principal (fun x1 x2 => x1 * x2) o

case inr
ho : 2 ≤ 2
⊢ Principal (fun x1 x2 => x1 * x2) 2

Proof state:
case inl.inl
o : Ordinal.{u}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
ho : o < 1
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
rw [lt_one_iff_zero.1 ho]

Result:
case inl.inl
o : Ordinal.{u}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
ho : o < 1
⊢ Principal (fun x1 x2 => x1 * x2) 0

Proof state:
case inl
o : Ordinal.{u}
ho✝ : o ≤ 2
ho : o ≤ 1
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
rcases lt_or_eq_of_le ho with (ho | rfl)

Result:
case inl.inl
o : Ordinal.{u}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
ho : o < 1
⊢ Principal (fun x1 x2 => x1 * x2) o

case inl.inr
ho✝ : 1 ≤ 2
ho : 1 ≤ 1
⊢ Principal (fun x1 x2 => x1 * x2) 1
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma chainTop_isNonZero' (hα' : genWeightSpace M α ≠ ⊥) :
    (chainTop α β).IsNonZero

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ genWeightSpace M α = ⊥

Tactic:
rw [← add_zero (α : L → R), ← e, genWeightSpace_add_chainTop _ _ hα]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ False

Tactic:
apply hα'

Result:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ genWeightSpace M α = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
⊢ (chainTop α β).IsNonZero

Tactic:
by_contra e

Result:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ False
-- Mathlib/RingTheory/Kaehler/TensorProduct.lean
@[local simp]
lemma mulActionBaseChange_smul_add (a : A) (x y : S ⊗[R] Ω[A⁄R]) :
    a • (x + y) = a • x + a • y

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) x) +
      (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) y) =
    a • x + a • y

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ a • (x + y) = a • x + a • y

Tactic:
show (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) (x + y)) = _

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) (x + y)) = a • x + a • y

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) (x + y)) = a • x + a • y

Tactic:
rw [map_add, smul_add, map_add]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) x) +
      (TensorProduct.comm R S (Ω[A⁄R])).symm (a • (TensorProduct.comm R S (Ω[A⁄R])) y) =
    a • x + a • y
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem eq_singleton_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty)
    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = {x} ∧ T = {x}

Proof state:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ y = x

Tactic:
exact (Set.prod_subset_iff.mp h_diag x (by simp only [hx, Set.mem_singleton]) y
  (by simp only [hy, Set.mem_singleton])).symm

Result:
no goals

Proof state:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ ∃ x, S = {x} ∧ T = {x}

Tactic:
refine ⟨x, ⟨hx, ?_⟩⟩

Result:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ T = {x}

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ y ∈ T

Tactic:
simp only [hy, Set.mem_singleton]

Result:
no goals

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ x ∈ S

Tactic:
simp only [hx, Set.mem_singleton]

Result:
no goals

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
⊢ ∃ x, S = {x} ∧ T = {x}

Tactic:
obtain ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ := eq_singleton_left_of_prod_subset_idRel hS hT h_diag,
  eq_singleton_right_prod_subset_idRel hS hT h_diag

Result:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ ∃ x, S = {x} ∧ T = {x}

Proof state:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ T = {x}

Tactic:
rw [hy, Set.singleton_eq_singleton_iff]

Result:
case intro.intro
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
x : X
hx : S = {x}
y : X
hy : T = {y}
⊢ y = x
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem cos_arg {x : ℂ} (hx : x ≠ 0) : Real.cos (arg x) = x.re / ‖x‖

Proof state:
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖

Tactic:
rw [Real.cos_add_pi, Real.cos_arcsin]

Result:
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -√(1 - ((-x).im / ‖x‖) ^ 2) = x.re / ‖x‖

Proof state:
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Tactic:
rw [Real.cos_sub_pi, Real.cos_arcsin]

Result:
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -√(1 - ((-x).im / ‖x‖) ^ 2) = x.re / ‖x‖

Proof state:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖

Tactic:
rw [Real.cos_arcsin]

Result:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ √(1 - (x.im / ‖x‖) ^ 2) = x.re / ‖x‖

Proof state:
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -√(1 - ((-x).im / ‖x‖) ^ 2) = x.re / ‖x‖

Tactic:
field_simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs,
  _root_.abs_of_neg (not_le.1 h₁), *]

Result:
no goals

Proof state:
x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.re / ‖x‖

Tactic:
split_ifs with h₁ h₂

Result:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (Real.arcsin (x.im / ‖x‖)) = x.re / ‖x‖

case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) + π) = x.re / ‖x‖

case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Proof state:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ √(1 - (x.im / ‖x‖) ^ 2) = x.re / ‖x‖

Tactic:
field_simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]

Result:
no goals

Proof state:
x : ℂ
hx : x ≠ 0
⊢ Real.cos x.arg = x.re / ‖x‖

Tactic:
rw [arg]

Result:
x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.re / ‖x‖

Proof state:
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -√(1 - ((-x).im / ‖x‖) ^ 2) = x.re / ‖x‖

Tactic:
field_simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs,
  _root_.abs_of_neg (not_le.1 h₁), *]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
theorem mem_exterior_singleton : x ∈ exterior {y} ↔ x ⤳ y

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ∈ exterior {y} ↔ x ⤳ y

Tactic:
rw [exterior_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_symm_eq_iff (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} :
    K.map e.symm = p ↔ p.map e = K

Proof state:
case mpr
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
⊢ map e.symm (map e p) = p

Tactic:
calc
  map e.symm (map e p) = comap e (map e p) := (comap_equiv_eq_map_symm _ _).symm
  _ = p := comap_map_eq_of_injective e.injective _

Result:
no goals

Proof state:
case mp
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map e (map e.symm K) = K

Tactic:
calc
  map e (map e.symm K) = comap e.symm (map e.symm K) := map_equiv_eq_comap_symm _ _
  _ = K := comap_map_eq_of_injective e.symm.injective _

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map e.symm K = p ↔ map e p = K

Tactic:
constructor <;> rintro rfl

Result:
case mp
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map e (map e.symm K) = K

case mpr
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
⊢ map e.symm (map e p) = p
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
/-- The First-Derivative Test from calculus, minima version,
expressed in terms of left and right filters. -/
lemma isLocalMin_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
    (hd₀ : ∀ᶠ x in 𝓝[<] b, DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ x in 𝓝[>] b, DifferentiableAt ℝ f x)
    (h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≥ 0) :
    IsLocalMin f b

Proof state:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
⊢ IsLocalMin f b

Tactic:
obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀

Result:
case intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMin f b

Proof state:
case intro.intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0
⊢ IsLocalMin f b

Tactic:
exact isLocalMin_of_deriv_Ioo ha.1 hc.1 h
  (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
  (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
  (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Result:
no goals

Proof state:
case intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMin f b

Tactic:
obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁

Result:
case intro.intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0
⊢ IsLocalMin f b