harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem toFunBilinear_apply_eq_sum (a : A) (p : R[X]) :
    toFunBilinear R A a p = p.sum fun n r => monomial n (a * algebraMap R A r)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ ((toFunBilinear R A) a) p = p.sum fun n r => (monomial n) (a * (algebraMap R A) r)

Tactic:
simp only [toFunBilinear_apply_apply, aeval_def, eval₂_eq_sum, Polynomial.sum, Finset.smul_sum]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ ∑ x ∈ p.support, a • ((algebraMap R A[X]) (p.coeff x) * X ^ x) =
    ∑ x ∈ p.support, (monomial x) (a * (algebraMap R A) (p.coeff x))

Proof state:
case e_f.h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
i : ℕ
⊢ a • ((algebraMap R A[X]) (p.coeff i) * X ^ i) = (monomial i) (a * (algebraMap R A) (p.coeff i))

Tactic:
rw [← Algebra.smul_def, ← C_mul', mul_smul_comm, C_mul_X_pow_eq_monomial, ← Algebra.commutes,
  ← Algebra.smul_def, smul_monomial]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ ∑ x ∈ p.support, a • ((algebraMap R A[X]) (p.coeff x) * X ^ x) =
    ∑ x ∈ p.support, (monomial x) (a * (algebraMap R A) (p.coeff x))

Tactic:
congr with i : 1

Result:
case e_f.h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
i : ℕ
⊢ a • ((algebraMap R A[X]) (p.coeff i) * X ^ i) = (monomial i) (a * (algebraMap R A) (p.coeff i))
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.as_sum (hp : p.Monic) :
    p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
this : C (p.coeff p.natDegree) = 1
⊢ C (p.coeff p.natDegree) * X ^ p.natDegree + ∑ x ∈ range p.natDegree, C (p.coeff x) * X ^ x =
    X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
rw [this, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ C (p.coeff p.natDegree) = 1

Tactic:
exact congr_arg C hp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ C (p.coeff p.natDegree) * X ^ p.natDegree + ∑ x ∈ range p.natDegree, C (p.coeff x) * X ^ x =
    X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ C (p.coeff p.natDegree) = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ C (p.coeff p.natDegree) * X ^ p.natDegree + ∑ x ∈ range p.natDegree, C (p.coeff x) * X ^ x =
    X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem transnumAuxSeq_dist_lt (n : ℕ) :
    dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Proof state:
case h
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) < 1

Tactic:
exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

Result:
no goals

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| < 1 / |2 ^ (n + 1)|

Tactic:
gcongr

Result:
case h
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) < 1

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Tactic:
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _

Result:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|

Tactic:
calc
  _ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| := by
    simp_rw [transnumAuxSeq, Real.dist_eq]
    rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
      pow_mul, sq, mul_apply]
  _ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

Result:
no goals

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) =
    dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|

Tactic:
simp_rw [transnumAuxSeq, Real.dist_eq]

Result:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| =
    |(f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0 - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| =
    |(f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0 - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|

Tactic:
rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
  pow_mul, sq, mul_apply]

Result:
no goals

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Tactic:
rw [div_div, ← pow_succ', ← abs_of_pos this]

Result:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem eventually_mul_left_iff (μ : Measure G) [IsMulLeftInvariant μ] (t : G) {p : G → Prop} :
    (∀ᵐ x ∂μ, p (t * x)) ↔ ∀ᵐ x ∂μ, p x

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ {x | p x} ∈ Filter.map (fun h => t * h) (ae μ)

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_mul_left_ae μ t]

Result:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ {x | p x} ∈ Filter.map (fun h => t * h) (ae μ)
-- Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
    IsPreimmersion (Spec.map f) ↔ IsEmbedding (PrimeSpectrum.comap f.hom) ∧
      f.hom.SurjectiveOnStalks

Proof state:
R S : CommRingCat
f : R ⟶ S
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f

Tactic:
exact RingHom.surjective_respectsIso

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ IsEmbedding ⇑(ConcreteCategory.hom (Spec.map f).base) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)

Tactic:
rfl

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Tactic:
haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by
  rw [← RingHom.toMorphismProperty_respectsIso_iff]
  exact RingHom.surjective_respectsIso

Result:
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Proof state:
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Tactic:
rw [← HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks), isPreimmersion_iff, and_comm]

Result:
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ IsEmbedding ⇑(ConcreteCategory.hom (Spec.map f).base) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)

Proof state:
R S : CommRingCat
f : R ⟶ S
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso

Tactic:
rw [← RingHom.toMorphismProperty_respectsIso_iff]

Result:
R S : CommRingCat
f : R ⟶ S
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem mul_iff (k : ℤ) (hk : k ≠ 0) :
    PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

Proof state:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

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

Result:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z

Proof state:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z

Tactic:
simp only [PythagoreanTriple]

Result:
x y z k : ℤ
hk : k ≠ 0
⊢ k * x * (k * x) + k * y * (k * y) = k * z * (k * z) → x * x + y * y = z * z

Proof state:
x y z k : ℤ
hk : k ≠ 0
⊢ k * x * (k * x) + k * y * (k * y) = k * z * (k * z) → x * x + y * y = z * z

Tactic:
intro h

Result:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ x * x + y * y = z * z

Proof state:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)

Tactic:
convert h using 1 <;> ring

Result:
no goals

Proof state:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ x * x + y * y = z * z

Tactic:
rw [← mul_left_inj' (mul_ne_zero hk hk)]

Result:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem repr_apply_apply (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι) :
    b.repr v i = ⟪b i, v⟫

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ b.repr v i = (starRingEnd 𝕜) 1 * b.repr v i

Tactic:
simp only [one_mul, eq_self_iff_true, map_one]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ b.repr v i = inner (b i) v

Tactic:
rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ b.repr v i = (starRingEnd 𝕜) 1 * b.repr v i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ b.repr v i = inner (b i) v

Tactic:
classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left]
  simp only [one_mul, eq_self_iff_true, map_one]

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem MellinConvergent.comp_rpow {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : a ≠ 0) :
    MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a)

Tactic:
refine Iff.trans ?_ (integrableOn_Ioi_comp_rpow_iff' _ ha)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ MellinConvergent (fun t => f (t ^ a)) s ↔
    IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ MellinConvergent (fun t => f (t ^ a)) s ↔
    IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume

Tactic:
rw [MellinConvergent]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ IntegrableOn (fun t => ↑t ^ (s - 1) • f (t ^ a)) (Ioi 0) volume ↔
    IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)

Tactic:
rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
  ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
  ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
  add_sub_assoc, sub_add_cancel]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ IntegrableOn (fun t => ↑t ^ (s - 1) • f (t ^ a)) (Ioi 0) volume ↔
    IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume

Tactic:
refine integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)
-- Mathlib/Data/Rat/Lemmas.lean
theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℚ) ↔ IsSquare n

Proof state:
n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem IsTerminal.strict_hom_ext (hI : IsTerminal I) {A : C} (f g : I ⟶ A) : f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this✝ : IsIso f
this : IsIso g
⊢ f = g

Tactic:
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this : IsIso f
⊢ f = g

Tactic:
haveI := hI.isIso_from g

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this✝ : IsIso f
this : IsIso g
⊢ f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
⊢ f = g

Tactic:
haveI := hI.isIso_from f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this : IsIso f
⊢ f = g
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mdifferentiableOn_iff_differentiableOn :
    MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
⊢ MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s

Tactic:
simp only [MDifferentiableOn, DifferentiableOn,
  mdifferentiableWithinAt_iff_differentiableWithinAt]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Basic.lean
theorem Normal.minpoly_eq_iff_mem_orbit [h : Normal F E] {x y : E} :
    minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
he : minpoly F x = minpoly F y
⊢ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Tactic:
obtain ⟨φ, hφ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp h) (he ▸ minpoly.aeval F x)

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
he : minpoly F x = minpoly F y
φ : E →ₐ[F] E
hφ : φ y = x
⊢ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
he : minpoly F x = minpoly F y
φ : E →ₐ[F] E
hφ : φ y = x
⊢ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Tactic:
exact ⟨AlgEquiv.ofBijective φ (φ.normal_bijective F E E), hφ⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
⊢ minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Tactic:
refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩

Result:
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
he : minpoly F x = minpoly F y
⊢ x ∈ MulAction.orbit (E ≃ₐ[F] E) y
-- Mathlib/Topology/Constructions.lean
theorem isClosedMap_sigmaMk {i : ι} : IsClosedMap (@Sigma.mk ι σ i)

Proof state:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsClosed s
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

Tactic:
rwa [preimage_image_eq _ sigma_mk_injective]

Result:
no goals

Proof state:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Result:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed ∅

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsClosedMap (Sigma.mk i)

Tactic:
intro s hs

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ IsClosed (Sigma.mk i '' s)

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Result:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsClosed s
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ IsClosed (Sigma.mk i '' s)

Tactic:
rw [isClosed_sigma_iff]

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ ∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))

Proof state:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed ∅

Tactic:
exact isClosed_empty

Result:
no goals

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ ∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))

Tactic:
intro j

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_idealRange (x : L) : f x ∈ idealRange f

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
x : L
⊢ f x ∈ LieIdeal.map f ⊤

Tactic:
exact LieIdeal.mem_map (LieSubmodule.mem_top x)

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
x : L
⊢ f x ∈ f.idealRange

Tactic:
rw [idealRange_eq_map]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
x : L
⊢ f x ∈ LieIdeal.map f ⊤
-- Mathlib/Data/Matroid/Restrict.lean
lemma Indep.augment_finset {I J : Finset α} (hI : M.Indep I) (hJ : M.Indep J)
    (hIJ : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e I)

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
x : α
hxI : M.Indep (insert x ↑I)
hx : x ∈ J ∧ x ∉ I
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Tactic:
exact ⟨x, hx.1, hx.2, hxI⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
⊢ (↑I).encard < (↑J).encard

Tactic:
simpa [encard_eq_coe_toFinset_card]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Tactic:
obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])

Result:
case intro.intro
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
x : α
hx : x ∈ ↑J \ ↑I
hxI : M.Indep (insert x ↑I)
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
x : α
hx : x ∈ ↑J \ ↑I
hxI : M.Indep (insert x ↑I)
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Tactic:
simp only [mem_diff, Finset.mem_coe] at hx

Result:
case intro.intro
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
x : α
hxI : M.Indep (insert x ↑I)
hx : x ∈ J ∧ x ∉ I
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_one {x : AddCircle T} : fourier 1 x = toCircle x

Proof state:
T : ℝ
x : AddCircle T
⊢ (fourier 1) x = ↑x.toCircle

Tactic:
rw [fourier_apply, one_zsmul]

Result:
no goals