harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Countable.lean
theorem countable_setOf_finite_subset {s : Set α} (hs : s.Countable) :
    { t | Set.Finite t ∧ t ⊆ s }.Countable

Proof state:
α : Type u
s : Set α
hs : s.Countable
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Tactic:
have := hs.to_subtype

Result:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Proof state:
case intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Set α
ht : t.Finite
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t

Tactic:
lift t to Set s using hts

Result:
case intro.intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Set ↑s
ht : (Subtype.val '' t).Finite
⊢ Subtype.val '' t ∈ range fun t => Subtype.val '' ↑t

Proof state:
case intro.intro.intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Finset ↑s
ht : (Subtype.val '' ↑t).Finite
⊢ Subtype.val '' ↑t ∈ range fun t => Subtype.val '' ↑t

Tactic:
exact mem_range_self _

Result:
no goals

Proof state:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Tactic:
refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_

Result:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t

Proof state:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t

Tactic:
rintro t ⟨ht, hts⟩

Result:
case intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Set α
ht : t.Finite
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t

Proof state:
case intro.intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Set ↑s
ht : (Subtype.val '' t).Finite
⊢ Subtype.val '' t ∈ range fun t => Subtype.val '' ↑t

Tactic:
lift t to Finset s using ht.of_finite_image Subtype.val_injective.injOn

Result:
case intro.intro.intro
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Finset ↑s
ht : (Subtype.val '' ↑t).Finite
⊢ Subtype.val '' ↑t ∈ range fun t => Subtype.val '' ↑t
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem is_const_of_fderivWithin_eq_zero (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0) (hx : x ∈ s) (hy : y ∈ s) : f x = f y

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0
⊢ f x = f y

Tactic:
simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm] using
  hs.norm_image_sub_le_of_norm_fderivWithin_le hf bound hx hy

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
x✝ y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0
hx✝ : x✝ ∈ s
hy : y ∈ s
x : E
hx : x ∈ s
⊢ ‖fderivWithin 𝕜 f s x‖ ≤ 0

Tactic:
simp only [hf' x hx, norm_zero, le_rfl]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
have bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0 := fun x hx => by
  simp only [hf' x hx, norm_zero, le_rfl]

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0
hx : x ∈ s
hy : y ∈ s
bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0
⊢ f x = f y
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Odd.strictMono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n

Proof state:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)

Tactic:
calc
  a ^ n + (c ^ n + d ^ n) = d ^ n := by
    rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]
  _ < c ^ n := pow_lt_pow_left₀ ?_ hd hn₀
  _ = b ^ n + (c ^ n + d ^ n) := by rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]

Result:
case inr.inr.intro.intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d < c

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False

Tactic:
simp [Odd, eq_comm (a := 0)] at hn

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem left_le_sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : f ≤ f.sup g h

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
⊢ f ≤ f.sup g h

Tactic:
refine ⟨le_sup_left, fun z₁ z₂ hz => ?_⟩

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ = ↑(f.sup g h) z₂

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ = ↑(f.sup g h) z₂

Tactic:
rw [← add_zero (f _), ← g.map_zero]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ + ↑g 0 = ↑(f.sup g h) z₂

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑z₁ + ↑0 = ↑z₂

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ + ↑g 0 = ↑(f.sup g h) z₂

Tactic:
refine (sup_apply h _ _ _ ?_).symm

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑z₁ + ↑0 = ↑z₂
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_absolutelyContinuous {m : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) :
    μ.withDensity f ≪ μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ (μ.withDensity f) s = 0

Tactic:
rw [withDensity_apply _ hs₁]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ μ.withDensity f ≪ μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ (μ.withDensity f) s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0

Tactic:
exact setLIntegral_measure_zero _ _ hs₂

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem succ_nth_conv'_eq_squashGCF_nth_conv' :
    g.convs' (n + 1) = (squashGCF g n).convs' n

Proof state:
case succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n✝ : ℕ
⊢ g.convs' (n✝ + 1 + 1) = (g.squashGCF (n✝ + 1)).convs' (n✝ + 1)

Tactic:
simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
  squashGCF]

Result:
no goals

Proof state:
case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

Tactic:
cases g_s_head_eq : g.s.get? 0 <;>
  simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]

Result:
no goals

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' (n + 1) = (g.squashGCF n).convs' n

Tactic:
cases n with
| zero =>
  cases g_s_head_eq : g.s.get? 0 <;>
    simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
| succ =>
  simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
    squashGCF]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Action/Basic.lean
theorem aeconst_of_forall_preimage_smul_ae_eq [SMul G α] [ErgodicSMul G α μ] {s : Set α}
    (hm : NullMeasurableSet s μ) (h : ∀ g : G, (g • ·) ⁻¹' s =ᵐ[μ] s) :
    EventuallyConst s (ae μ)

Proof state:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
g : G
⊢ (fun x => g • x) ⁻¹' t =ᶠ[ae μ] (fun x => g • x) ⁻¹' s

Tactic:
exact tendsto_smul_ae _ _ hst.symm

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
rcases hm with ⟨t, htm, hst⟩

Result:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst s (ae μ)

Proof state:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst s (ae μ)

Tactic:
refine .congr ?_ hst.symm

Result:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst t (ae μ)

Proof state:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst t (ae μ)

Tactic:
refine ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_

Result:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
g : G
⊢ (fun x => g • x) ⁻¹' t =ᶠ[ae μ] t

Proof state:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
g : G
⊢ (fun x => g • x) ⁻¹' t =ᶠ[ae μ] t

Tactic:
refine .trans (.trans ?_ (h g)) hst

Result:
case intro.intro
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
g : G
⊢ (fun x => g • x) ⁻¹' t =ᶠ[ae μ] (fun x => g • x) ⁻¹' s
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem isSymmetric_adjoint_mul_self (T : E →ₗ[𝕜] E) : IsSymmetric (LinearMap.adjoint T * T)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x y : E
⊢ ⟪(adjoint T * T) x, y⟫_𝕜 = ⟪x, (adjoint T * T) y⟫_𝕜

Tactic:
simp only [mul_apply, adjoint_inner_left, adjoint_inner_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ (adjoint T * T).IsSymmetric

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x y : E
⊢ ⟪(adjoint T * T) x, y⟫_𝕜 = ⟪x, (adjoint T * T) y⟫_𝕜
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem dyadicMap_apply_pow (m : ℤ) (n : ℕ) :
    dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) =
      m • powHalf n

Proof state:
m : ℤ
n : ℕ
⊢ ↑m * powHalf n = m • powHalf n

Tactic:
simp only [zsmul_eq_mul]

Result:
no goals

Proof state:
m : ℤ
n : ℕ
⊢ dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • powHalf n

Tactic:
rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]

Result:
m : ℤ
n : ℕ
⊢ ↑m * powHalf n = m • powHalf n
-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
private lemma coroot_eq_coreflection_of_root_eq' [CharZero R] [NoZeroSMulDivisors R M]
    (p : PerfectPairing R M N)
    (root : ι ↪ M)
    (coroot : ι ↪ N)
    (hp : ∀ i, p (root i) (coroot i) = 2)
    (hr : ∀ i, MapsTo (preReflection (root i) (p.flip (coroot i))) (range root) (range root))
    (hc : ∀ i, MapsTo (preReflection (coroot i) (p (root i))) (range coroot) (range coroot))
    {i j k : ι} (hk : root k = preReflection (root i) (p.flip (coroot i)) (root j)) :
    coroot k = preReflection (coroot i) (p (root i)) (coroot j)

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
hk₀ : root k ≠ 0
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
⊢ coroot k = coroot l

Tactic:
have hkl : (p.flip (coroot l)) (root k) = 2 := by
  simp only [hl, preReflection_apply, hk, PerfectPairing.flip_apply_apply, map_sub, hp j,
    map_smul, smul_eq_mul, hp i, mul_sub, sα, α, α', β, mul_two, mul_add, LinearMap.sub_apply,
    LinearMap.smul_apply]
  rw [mul_comm (p (root i) (coroot j))]
  abel

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
hk₀ : root k ≠ 0
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
⊢ coroot k = coroot l
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem liftpPreservation_iff_uniform : q.LiftPPreservation ↔ q.IsUniform

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation ↔ IsUniform

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem norm_sub_le_of_geometric_bound_of_hasSum (hr : r < 1) (hf : ∀ n, ‖f n‖ ≤ C * r ^ n) {a : α}
    (ha : HasSum f a) (n : ℕ) : ‖(∑ x ∈ Finset.range n, f x) - a‖ ≤ C * r ^ n / (1 - r)

Proof state:
case ha
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)

Tactic:
exact ha.tendsto_sum_nat

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)

Tactic:
rw [← dist_eq_norm]

Result:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)

Tactic:
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)

Result:
case ha
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gaugeRescale_gaugeRescale {s t u : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t)
    (x : E) : gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Proof state:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Proof state:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t x ≠ 0

case inr.hc
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ 0 ≤ gauge s x / gauge t x

Tactic:
exacts [((gauge_pos hta htb).2 hx).ne', div_nonneg (gauge_nonneg _) (gauge_nonneg _)]

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul,
  div_mul_div_cancel₀]

Result:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t x ≠ 0

case inr.hc
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ 0 ≤ gauge s x / gauge t x
-- Mathlib/Algebra/Order/SuccPred.lean
theorem wcovBy_add_one (x : α) : x ⩿ x + 1

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ x + 1

Tactic:
rw [← succ_eq_add_one]

Result:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ succ x

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ succ x

Tactic:
exact wcovBy_succ x

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2

Proof state:
x : ℂ
⊢ cos x ^ 2 = 1 / 2 + cos (2 * x) / 2

Tactic:
simp [cos_two_mul, div_add_div_same, mul_div_cancel_left₀, two_ne_zero, -one_div]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
lemma factorPowSucc.isUnit_of_isUnit_image {n : ℕ} (npos : n > 0) {a : R ⧸ I ^ (n + 1)}
    (h : IsUnit (factorPow I n.le_succ a)) : IsUnit a

Proof state:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ c ∈ I ^ (n - 1) * I ^ 1

Tactic:
simpa only [← pow_add, Nat.sub_add_cancel npos] using hc

Result:
no goals