harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/W/Constructions.lean
theorem leftInverse_nat : Function.LeftInverse ofNat toNat
  | WType.mk Natα.zero f => by
    rw [toNat, ofNat]
    congr
    ext x
    cases x
  | WType.mk Natα.succ f => by
    simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
    rfl

Proof state:
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f

Tactic:
ext x

Result:
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ x.elim = f x

Proof state:
f : Natβ Natα.zero → WType Natβ
⊢ ofNat (mk Natα.zero f).toNat = mk Natα.zero f

Tactic:
rw [toNat, ofNat]

Result:
f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f

Proof state:
f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f

Tactic:
congr

Result:
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f

Proof state:
f : Natβ Natα.succ → WType Natβ
⊢ ofNat (mk Natα.succ f).toNat = mk Natα.succ f

Tactic:
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]

Result:
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f

Proof state:
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ x.elim = f x

Tactic:
cases x

Result:
no goals

Proof state:
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
@[simp]
lemma one_sub_mul_self (h : IsIdempotentElem a) : (1 - a) * a = 0

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ (1 - a) * a = 0

Tactic:
rw [sub_mul, one_mul, h.eq, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UInt.lean
theorem USize.le_size : 2 ^ 32 ≤ USize.size

Proof state:
⊢ 32 ≤ System.Platform.numBits

Tactic:
cases System.Platform.numBits_eq <;> simp_arith [*]

Result:
no goals

Proof state:
⊢ 2 ^ 32 ≤ 2 ^ System.Platform.numBits

Tactic:
apply Nat.pow_le_pow_of_le_right (by decide)

Result:
⊢ 32 ≤ System.Platform.numBits

Proof state:
⊢ 2 > 0

Tactic:
decide

Result:
no goals

Proof state:
⊢ 2 ^ 32 ≤ size

Tactic:
rw [size_eq]

Result:
⊢ 2 ^ 32 ≤ 2 ^ System.Platform.numBits
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_monomial_mul (a : R) :
    coeff R m (monomial R n a * φ) = if n ≤ m then a * coeff R (m - n) φ else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) ((monomial R n) a) * (coeff R p.2) φ ≠ 0 → p.1 = n
⊢ (if n ≤ m then ∑ x ∈ {(n, m - n)}, (coeff R x.1) ((monomial R n) a) * (coeff R x.2) φ
    else ∑ x ∈ ∅, (coeff R x.1) ((monomial R n) a) * (coeff R x.2) φ) =
    if n ≤ m then a * (coeff R (m - n)) φ else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R m) ((monomial R n) a * φ) = if n ≤ m then a * (coeff R (m - n)) φ else 0

Tactic:
classical
have :
  ∀ p ∈ antidiagonal m,
    coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial R n a) * coeff R p.2 φ ≠ 0 → p.1 = n :=
  fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
  Finset.sum_ite_index]
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R m) ((monomial R n) a * φ) = if n ≤ m then a * (coeff R (m - n)) φ else 0

Tactic:
have :
  ∀ p ∈ antidiagonal m,
    coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial R n a) * coeff R p.2 φ ≠ 0 → p.1 = n :=
  fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) ((monomial R n) a) * (coeff R p.2) φ ≠ 0 → p.1 = n
⊢ (coeff R m) ((monomial R n) a * φ) = if n ≤ m then a * (coeff R (m - n)) φ else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) ((monomial R n) a) * (coeff R p.2) φ ≠ 0 → p.1 = n
⊢ (coeff R m) ((monomial R n) a * φ) = if n ≤ m then a * (coeff R (m - n)) φ else 0

Tactic:
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
  Finset.sum_ite_index]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) ((monomial R n) a) * (coeff R p.2) φ ≠ 0 → p.1 = n
⊢ (if n ≤ m then ∑ x ∈ {(n, m - n)}, (coeff R x.1) ((monomial R n) a) * (coeff R x.2) φ
    else ∑ x ∈ ∅, (coeff R x.1) ((monomial R n) a) * (coeff R x.2) φ) =
    if n ≤ m then a * (coeff R (m - n)) φ else 0
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight [Nontrivial R]
    {B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Basis n R M} (h : B.IsOrthoᵢ v) (hB : B.SeparatingRight)
    (i : n) : ¬B.IsOrtho (v i) (v i)

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ ¬B.IsOrtho (v i) (v i)

Tactic:
rw [isOrthoᵢ_flip] at h

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
v : Basis n R M
h : B.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ ¬B.IsOrtho (v i) (v i)

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
v : Basis n R M
h : B.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ ¬B.IsOrtho (v i) (v i)

Tactic:
rw [isOrtho_flip]

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
v : Basis n R M
h : B.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ ¬B.flip.IsOrtho (v i) (v i)

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
v : Basis n R M
h : B.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ ¬B.flip.IsOrtho (v i) (v i)

Tactic:
exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem lift_map (h : IsAdjoinRoot S f) (z : R[X]) : h.lift i x hx (h.map z) = z.eval₂ i x

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ (lift i x h hx) (h.map z) = eval₂ i x z

Tactic:
rw [lift, RingHom.coe_mk]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ { toFun := fun z => eval₂ i x (h.repr z), map_one' := ⋯, map_mul' := ⋯ } (h.map z) = eval₂ i x z

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ eval₂ i x (h.repr (h.map z)) = eval₂ i x z

Tactic:
rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ { toFun := fun z => eval₂ i x (h.repr z), map_one' := ⋯, map_mul' := ⋯ } (h.map z) = eval₂ i x z

Tactic:
dsimp

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : R[X]
⊢ eval₂ i x (h.repr (h.map z)) = eval₂ i x z
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_left_add_left (m n k : ℕ) : gcd (n * k + m) n = gcd m n

Proof state:
m n k : ℕ
⊢ (n * k + m).gcd n = m.gcd n

Tactic:
rw [gcd_comm, gcd_mul_left_add_right, gcd_comm]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma isCoprime_helper {r s t w : 𝓞 K} (hr : ¬ λ ∣ r) (hs : ¬ λ ∣ s)
    (Hp : ∀ {p}, Prime p → p ∣ t → p ∣ w → Associated p λ) (H₁ : ∀ {q}, q ∣ r → q ∣ t)
    (H₂ : ∀ {q}, q ∣ s → q ∣ w) : IsCoprime r s

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
r s t w : 𝓞 K
hr : ¬λ ∣ r
hs : ¬λ ∣ s
Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ
H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t
H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w
⊢ IsCoprime r s

Tactic:
refine isCoprime_of_prime_dvd (not_and.2 (fun _ hz ↦ hs (by simp [hz])))
  (fun p hp p_dvd_r p_dvd_s ↦ hr ?_)

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
r s t w : 𝓞 K
hr : ¬λ ∣ r
hs : ¬λ ∣ s
Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ
H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t
H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w
p : 𝓞 K
hp : Prime p
p_dvd_r : p ∣ r
p_dvd_s : p ∣ s
⊢ λ ∣ r

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
r s t w : 𝓞 K
hr : ¬λ ∣ r
hs : ¬λ ∣ s
Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ
H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t
H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w
p : 𝓞 K
hp : Prime p
p_dvd_r : p ∣ r
p_dvd_s : p ∣ s
⊢ λ ∣ r

Tactic:
rwa [← Associated.dvd_iff_dvd_left <| Hp hp (H₁ p_dvd_r) (H₂ p_dvd_s)]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
r s t w : 𝓞 K
hr : ¬λ ∣ r
hs : ¬λ ∣ s
Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ
H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t
H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w
x✝ : r = 0
hz : s = 0
⊢ λ ∣ s

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem sub_conj (z : K) : z - conj z = 2 * im z * I :=
  calc
    z - conj z = re z + im z * I - (re z - im z * I)

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z - (starRingEnd K) z = ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I)

Tactic:
rw [re_add_im, ← conj_eq_re_sub_im]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I) = 2 * ↑(im z) * I

Tactic:
rw [add_sub_sub_cancel, ← two_mul, mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/MorphismProperty.lean
/-- A reformulation of `CategoryTheory.Paths.induction` in terms of `MorphismProperty`. -/
lemma morphismProperty_eq_top
    (P : MorphismProperty (Paths V))
    (id : ∀ {v : V}, P (𝟙 (of.obj v)))
    (comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)) :
    P = ⊤

Proof state:
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
⊢ P = ⊤

Tactic:
ext

Result:
case h
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝

Proof state:
case h.mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
exact fun _ ↦ induction (fun f ↦ P f) id comp _

Result:
no goals

Proof state:
case h.mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝

Tactic:
constructor

Result:
case h.mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

case h.mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (p ≫ of.map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[reassoc (attr := simp)]
lemma residueFieldCongr_fromSpecResidueField {x y : X} (h : x = y) :
    Spec.map (X.residueFieldCongr h).hom ≫ X.fromSpecResidueField _ =
      X.fromSpecResidueField _

Proof state:
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x = y
⊢ Spec.map (residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y

Tactic:
subst h

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ici_mul_Ioi_subset' (a b : α) : Ici a * Ioi b ⊆ Ioi (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ioi b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioi (a * b)

Tactic:
exact mul_lt_mul_of_le_of_lt hya hzb

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Ici a * Ioi b ⊆ Ioi (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ioi b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioi (a * b)
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C)
    (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) : RespectsIso P where
  precomp {X Y Z} e (he : IsIso e) f hf

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ (Iso.refl (Arrow.mk f).right).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ P (e ≫ f)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ (Iso.refl (Arrow.mk f).right).hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_fin_succ {n} {v : Fin (n + 1) → V} :
    LinearIndependent K v ↔
      LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (range <| Fin.tail v)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
v : Fin (n + 1) → V
⊢ LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ span K (range (Fin.tail v))

Tactic:
rw [← linearIndependent_fin_cons, Fin.cons_self_tail]

Result:
no goals
-- Mathlib/Condensed/Light/TopCatAdjunction.lean
lemma continuous_coinducingCoprod {S : LightProfinite.{u}} (x : X.val.obj ⟨S⟩) :
    Continuous fun a ↦ (X.coinducingCoprod ⟨⟨S, x⟩, a⟩)

Proof state:
X : LightCondSet
S : LightProfinite
x : X.val.obj (Opposite.op S)
⊢ Continuous fun a => LightCondSet.coinducingCoprod X ⟨⟨S, x⟩, a⟩

Tactic:
suffices ∀ (i : (T : LightProfinite.{u}) × X.val.obj ⟨T⟩),
    Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩

Result:
X : LightCondSet
S : LightProfinite
x : X.val.obj (Opposite.op S)
⊢ ∀ (i : (T : LightProfinite) × X.val.obj (Opposite.op T)), Continuous fun a => LightCondSet.coinducingCoprod X ⟨i, a⟩

Proof state:
X : LightCondSet
S : LightProfinite
x : X.val.obj (Opposite.op S)
⊢ Continuous (LightCondSet.coinducingCoprod X)

Tactic:
apply continuous_coinduced_rng

Result:
no goals

Proof state:
X : LightCondSet
S : LightProfinite
x : X.val.obj (Opposite.op S)
⊢ ∀ (i : (T : LightProfinite) × X.val.obj (Opposite.op T)), Continuous fun a => LightCondSet.coinducingCoprod X ⟨i, a⟩

Tactic:
rw [← continuous_sigma_iff]

Result:
X : LightCondSet
S : LightProfinite
x : X.val.obj (Opposite.op S)
⊢ Continuous (LightCondSet.coinducingCoprod X)
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem disjoint_def {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1 :=
  disjoint_iff_inf_le.trans <| by simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

Tactic:
simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_retraction_subtype_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s)
    (hne : s.Nonempty) :
    ∃ f : (∀ n, E n) → s, (∀ x : s, f x = x) ∧ Surjective f ∧ Continuous f

Proof state:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1

Tactic:
have A : ∀ x : range f, rangeFactorization f x = x := fun x ↦ Subtype.eq <| fs x x.2

Result:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1

Proof state:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1

Tactic:
exact ⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩

Result:
no goals

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
⊢ ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f

Tactic:
obtain ⟨f, fs, rfl, f_cont⟩ :
  ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
  exists_retraction_of_isClosed hs hne

Result:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous f
hs : IsClosed (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
⊢ ∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma evalEval_baseChange_polynomial_X_Y :
    (W'.baseChange R[X][Y]).toAffine.polynomial.evalEval (C X) Y = W'.polynomial

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ evalEval (C X) Y (baseChange W' R[X][Y]).toAffine.polynomial = W'.polynomial

Tactic:
rw [map_polynomial, evalEval, eval_map, eval_C_X_eval₂_map_C_X]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem leadingCoeff_map' (hf : Injective f) (p : R[X]) :
    leadingCoeff (p.map f) = f (leadingCoeff p)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)

Tactic:
rw [coeff_map, natDegree_map_eq_of_injective hf p]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
unfold leadingCoeff

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)