harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem map_pow_ne_zero (f_nonneg : 0 ≤ f) {x : R} (hx : IsUnit x) (hfx : f x ≠ 0) (n : ℕ)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) : f (x ^ n) ≠ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ False

Tactic:
have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ f (x ^ n) ≠ 0

Tactic:
have h1 : f 1 ≠ 0 := map_one_ne_zero (Function.ne_iff.mpr ⟨x, hfx⟩) f_nonneg f_mul

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
⊢ f (x ^ n) ≠ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
⊢ f (x ^ n) ≠ 0

Tactic:
intro hxn

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ f 1 ≤ 0

Tactic:
simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False

Tactic:
exact h1 <| this.antisymm (f_nonneg 1)

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem memberSubfamily_nonMemberSubfamily : (𝒜.nonMemberSubfamily a).memberSubfamily a = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (nonMemberSubfamily a 𝒜) = ∅

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ ∅

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem basisFun_repr (x : η → R) (i : η) : (Pi.basisFun R η).repr x i = x i

Proof state:
R : Type u_1
η : Type u_2
inst✝¹ : Semiring R
inst✝ : Finite η
x : η → R
i : η
⊢ ((basisFun R η).repr x) i = x i

Tactic:
simp [basisFun]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
  | 0, _ => by simp [Nat.div_zero, n.zero_le]
  | succ k, h => by
    suffices succ k * (m / succ k) ≤ succ k * n from
      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
    have h2 : m % succ k + succ k * (m / succ k) = m

Proof state:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Tactic:
have h3 : m ≤ succ k * n := h

Result:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
h3 : m ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Proof state:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
h3 : m ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Tactic:
rw [← h2] at h3

Result:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
h3 : m % k.succ + k.succ * (m / k.succ) ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Proof state:
m n k : Nat
h : m ≤ k.succ * n
⊢ m / k.succ ≤ n

Tactic:
suffices succ k * (m / succ k) ≤ succ k * n from
  Nat.le_of_mul_le_mul_left this (zero_lt_succ _)

Result:
m n k : Nat
h : m ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Proof state:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
⊢ m % k.succ + k.succ * (m / k.succ) = m

Tactic:
rw [mod_add_div]

Result:
no goals

Proof state:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
h3 : m % k.succ + k.succ * (m / k.succ) ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Tactic:
exact Nat.le_trans h1 h3

Result:
no goals

Proof state:
m n : Nat
x✝ : m ≤ 0 * n
⊢ m / 0 ≤ n

Tactic:
simp [Nat.div_zero, n.zero_le]

Result:
no goals

Proof state:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Tactic:
have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]

Result:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
h2 : m % k.succ + k.succ * (m / k.succ) = m
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Proof state:
m n k : Nat
h : m ≤ k.succ * n
⊢ k.succ * (m / k.succ) ≤ k.succ * n

Tactic:
have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _

Result:
m n k : Nat
h : m ≤ k.succ * n
h1 : k.succ * (m / k.succ) ≤ m % k.succ + k.succ * (m / k.succ)
⊢ k.succ * (m / k.succ) ≤ k.succ * n
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation.map_one' : v.intValuationDef 1 = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1

Tactic:
rw [v.intValuationDef_if_neg (zero_ne_one.symm : (1 : R) ≠ 0), Ideal.span_singleton_one, ←
  Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
  Associates.count_zero (by apply v.associates_irreducible), Int.ofNat_zero, neg_zero, ofAdd_zero,
  WithZero.coe_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1

Tactic:
classical
rw [v.intValuationDef_if_neg (zero_ne_one.symm : (1 : R) ≠ 0), Ideal.span_singleton_one, ←
  Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
  Associates.count_zero (by apply v.associates_irreducible), Int.ofNat_zero, neg_zero, ofAdd_zero,
  WithZero.coe_one]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem erase_le_iff_le_cons {s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t :=
  ⟨fun h => le_trans (le_cons_erase _ _) (cons_le_cons _ h), fun h =>
    if m : a ∈ s then by rw [← cons_erase m] at h; exact (cons_le_cons_iff _).1 h
    else le_trans (erase_le _ _) ((le_cons_of_not_mem m).1 h)⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
exact (cons_le_cons_iff _).1 h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
rw [← cons_erase m] at h

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
-- Mathlib/Algebra/Polynomial/Monic.lean
lemma irreducible_of_monic (hp : p.Monic) (hp1 : p ≠ 1) :
    Irreducible p ↔ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

Proof state:
case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * C f.leadingCoeff * (f * C g.leadingCoeff) = p

Tactic:
rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
  mul_comm, ← hfg]

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).Monic

Tactic:
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).Monic

Tactic:
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

Tactic:
refine
  ⟨fun h f g hf hg hp => (h.2 f g hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
    ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
      (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
        (isUnit_of_mul_eq_one f _)
        (isUnit_of_mul_eq_one g _)⟩⟩

Result:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).Monic

case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).Monic

case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * C f.leadingCoeff * (f * C g.leadingCoeff) = p
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (u * X ω)` is integrable at `u ≤ 0`, then it is integrable on `[u, 0]`. -/
lemma integrable_exp_mul_of_nonpos_of_ge [IsFiniteMeasure μ]
    (hu : Integrable (fun ω ↦ exp (u * X ω)) μ) (h_nonpos : t ≤ 0) (htu : u ≤ t) :
    Integrable (fun ω ↦ exp (t * X ω)) μ :=
  integrable_exp_mul_of_le_of_le hu (by simp) htu h_nonpos

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
inst✝ : IsFiniteMeasure μ
hu : Integrable (fun ω => rexp (u * X ω)) μ
h_nonpos : t ≤ 0
htu : u ≤ t
⊢ Integrable (fun ω => rexp (0 * X ω)) μ

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_mem_Ioc_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1)) :=
  let ⟨m, hle, hlt⟩ := exists_mem_Ico_zpow (inv_pos.2 hx) hy
  have hyp : 0 < y := lt_trans zero_lt_one hy
  ⟨-(m + 1), by rwa [zpow_neg, inv_lt_comm₀ (zpow_pos hyp _) hx], by
    rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]⟩

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x

Tactic:
rwa [zpow_neg, inv_lt_comm₀ (zpow_pos hyp _) hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-(m + 1) + 1)

Tactic:
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).darts = p.darts

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).darts = p.darts

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).darts = p.darts

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).darts = p.darts
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem extend_unique (hf : UniformContinuous f) {g : hatα → β} (hg : UniformContinuous g)
    (h : ∀ a : α, f a = g (ι a)) : pkg.extend f = g

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)

Tactic:
simpa only [pkg.extend_coe hf] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ pkg.extend f = g

Tactic:
apply pkg.funext pkg.continuous_extend hg.continuous

Result:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx = b.denote ctx) = (c.denote ctx = d.denote ctx)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : (denote ctx c = denote ctx d) = (denote ctx a = denote ctx b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Tactic:
exact this.symm

Result:
no goals

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_eq ctx (c.toPoly, d.toPoly) = Poly.denote_eq ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Tactic:
simp [toNormPoly, Poly.norm, Poly.denote_eq, -eq_iff_iff] at this

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : (denote ctx c = denote ctx d) = (denote ctx a = denote ctx b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Tactic:
have := Poly.denote_eq_cancel_eq ctx a.toNormPoly b.toNormPoly

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_eq ctx (a.toNormPoly.cancel b.toNormPoly) = Poly.denote_eq ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_eq ctx (a.toNormPoly.cancel b.toNormPoly) = Poly.denote_eq ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

Tactic:
rw [h] at this

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_eq ctx (c.toPoly, d.toPoly) = Poly.denote_eq ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive (attr := simp)]
lemma stabilizer_smul_eq_right {α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
    stabilizer G (a • b) = stabilizer G b :=
  (le_stabilizer_smul_right _ _).antisymm' <| (le_stabilizer_smul_right a⁻¹ _).trans_eq <| by
    rw [inv_smul_smul]

Proof state:
G : Type u_1
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G β
α : Type u_4
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : SMulCommClass G α β
a : α
b : β
⊢ stabilizer G (a⁻¹ • a • b) = stabilizer G b

Tactic:
rw [inv_smul_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem flat_of_preservesFiniteLimits [HasFiniteLimits C] (F : C ⥤ D) [PreservesFiniteLimits F] :
    RepresentablyFlat F :=
  ⟨fun X =>
    haveI : HasFiniteLimits (StructuredArrow X F)

Proof state:
case has_limit
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ autoParam (∀ (F_1 : J ⥤ StructuredArrow X F), HasLimit F_1) _auto✝

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ HasFiniteLimits (StructuredArrow X F)

Tactic:
apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ HasLimitsOfShape J (StructuredArrow X F)

Tactic:
constructor

Result:
case has_limit
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ autoParam (∀ (F_1 : J ⥤ StructuredArrow X F), HasLimit F_1) _auto✝

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)

Tactic:
intro J sJ fJ

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ HasLimitsOfShape J (StructuredArrow X F)
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Ici : (fun x => x - a) '' Ici b = Ici (b - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) '' Ici b = Ici (b - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma norm_eq_max_natAbs (x : Fin 2 → ℤ) : ‖x‖ = max (x 0).natAbs (x 1).natAbs

Proof state:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = ↑(x 0).natAbs ⊔ ↑(x 1).natAbs

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Result:
x : Fin 2 → ℤ
c : NNReal
⊢ ‖x‖₊ ≤ c ↔ ↑(x 0).natAbs ⊔ ↑(x 1).natAbs ≤ c

Proof state:
x : Fin 2 → ℤ
c : NNReal
⊢ ‖x‖₊ ≤ c ↔ ↑(x 0).natAbs ⊔ ↑(x 1).natAbs ≤ c

Tactic:
simp only [pi_nnnorm_le_iff, Fin.forall_fin_two, max_le_iff, NNReal.natCast_natAbs]

Result:
no goals

Proof state:
x : Fin 2 → ℤ
⊢ ‖x‖ = ↑((x 0).natAbs ⊔ (x 1).natAbs)

Tactic:
rw [← coe_nnnorm, ← NNReal.coe_natCast, NNReal.coe_inj, Nat.cast_max]

Result:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = ↑(x 0).natAbs ⊔ ↑(x 1).natAbs
-- Mathlib/Control/LawfulFix.lean
theorem le_f_of_mem_approx {x} : x ∈ approxChain f → x ≤ f x

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ ∀ (x_1 : ℕ), x = (approxChain f) x_1 → x ≤ f x

Tactic:
rintro i rfl

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ (approxChain f) i ≤ f ((approxChain f) i)

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ f x

Tactic:
simp only [Membership.mem, forall_exists_index]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ ∀ (x_1 : ℕ), x = (approxChain f) x_1 → x ≤ f x

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ (approxChain f) i ≤ f ((approxChain f) i)

Tactic:
apply approx_mono'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
    l.toArray.all p 0 stop = l.all p

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
l : List α
h : stop = l.toArray.size
⊢ l.toArray.all p 0 stop = l.all p

Tactic:
subst h

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.all p = l.all p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.all p = l.all p

Tactic:
rw [all_toList]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_coe_re_add_coe_im {f : X → 𝕜} (hf : Integrable f μ) :
    ∫ x, (re (f x) : 𝕜) ∂μ + (∫ x, (im (f x) : 𝕜) ∂μ) * RCLike.I = ∫ x, f x ∂μ

Proof state:
case hg
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun a => I • ↑(im (f a))) μ

Tactic:
exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (a : X), ↑(re (f a)) + I • ↑(im (f a)) ∂μ = ∫ (x : X), f x ∂μ

Tactic:
congr

Result:
case e_f
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ (fun a => ↑(re (f a)) + I • ↑(im (f a))) = fun x => f x

Proof state:
case e_f.h
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
⊢ ↑(re (f x)) + I • ↑(im (f x)) = f x

Tactic:
rw [smul_eq_mul, mul_comm, RCLike.re_add_im]

Result:
no goals

Proof state:
case hf
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x => ↑(re (f x))) μ

Tactic:
exact hf.re.ofReal

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + (∫ (x : X), ↑(im (f x)) ∂μ) * I = ∫ (x : X), f x ∂μ

Tactic:
rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]

Result:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (a : X), ↑(re (f a)) + I • ↑(im (f a)) ∂μ = ∫ (x : X), f x ∂μ

case hf
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x => ↑(re (f x))) μ

case hg
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun a => I • ↑(im (f a))) μ

Proof state:
case e_f
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ (fun a => ↑(re (f a)) + I • ↑(im (f a))) = fun x => f x

Tactic:
ext1 x

Result:
case e_f.h
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
⊢ ↑(re (f x)) + I • ↑(im (f x)) = f x