harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Presentation.lean
private lemma aux_ker :
    RingHom.ker (Q.aux P) = Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Proof state:
case hf
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Function.Bijective ⇑↑(sumAlgEquiv R Q.vars P.vars)

Tactic:
simpa using AlgEquiv.bijective (sumAlgEquiv R Q.vars P.vars)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Ideal.comap (↑(sumAlgEquiv R Q.vars P.vars))
      (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial P.vars R) (MvPolynomial Q.vars (MvPolynomial P.vars R)))
        (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Tactic:
rw [← sumAlgEquiv_comp_rename_inr, ← Ideal.map_mapₐ, Ideal.comap_map_of_bijective]

Result:
case hf
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Function.Bijective ⇑↑(sumAlgEquiv R Q.vars P.vars)

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ RingHom.ker (Algebra.Presentation.aux Q P) = Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Tactic:
rw [aux_eq_comp, ← AlgHom.comap_ker, MvPolynomial.ker_mapAlgHom]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Ideal.comap (↑(sumAlgEquiv R Q.vars P.vars)) (Ideal.map C (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Ideal.comap (↑(sumAlgEquiv R Q.vars P.vars)) (Ideal.map C (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Tactic:
show Ideal.comap _ (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial P.vars R) _) _) = _

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Ideal.comap (↑(sumAlgEquiv R Q.vars P.vars))
      (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial P.vars R) (MvPolynomial Q.vars (MvPolynomial P.vars R)))
        (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma exists_eventually_const_mul_le_r :
    ∃ c ∈ Set.Ioo (0 : ℝ) 1, ∀ᶠ (n : ℕ) in atTop, ∀ i, c * n ≤ r i n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

Tactic:
have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ 0 < b (min_bi b) / 2

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

Tactic:
exact ⟨b (min_bi b) / 2, ⟨⟨by positivity, R.bi_min_div_two_lt_one⟩, R.eventually_bi_mul_le_r⟩⟩

Result:
no goals
-- Mathlib/Probability/Distributions/Geometric.lean
/-- The geometric pmf is measurable. -/
@[measurability]
lemma measurable_geometricPMFReal : Measurable (geometricPMFReal p)

Proof state:
p : ℝ
⊢ Measurable (geometricPMFReal p)

Tactic:
measurability

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem eq_cosets_of_normal (N : s.Normal) (g : α) : g • (s : Set α) = op g • s :=
  Set.ext fun a => by simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : s.Normal
g a : α
⊢ a ∈ g • ↑s ↔ a ∈ op g • ↑s

Tactic:
simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ σ) s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
  hfg.sum_smul_comp_perm_le_sum_smul hσ]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem inv_Ioi₀ {a : α} (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : 0 < a
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹

Tactic:
rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ici_iff_integrableOn_Ioi :
    IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ :=
  integrableOn_Ici_iff_integrableOn_Ioi' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ μ {b} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_zero_left (x : E) : ⟪0, x⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪0, x⟫_𝕜 = 0

Tactic:
rw [← zero_smul 𝕜 (0 : E), inner_smul_left, RingHom.map_zero, zero_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_attach (s : Finset α) (f : α → β) : ∏ x ∈ s.attach, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

Tactic:
classical rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

Tactic:
rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]

Result:
no goals
-- Mathlib/Algebra/Group/Equiv/Defs.lean
@[to_additive (attr := simp)]
lemma coe_monoidHom_symm_comp_coe_monoidHom (e : M ≃* N) :
    (e.symm : N →* M).comp e = MonoidHom.id _

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e.symm).comp ↑e = MonoidHom.id M

Tactic:
ext

Result:
case h
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : M
⊢ ((↑e.symm).comp ↑e) x✝ = (MonoidHom.id M) x✝

Proof state:
case h
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : M
⊢ ((↑e.symm).comp ↑e) x✝ = (MonoidHom.id M) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.completion_id :
    (NormedAddGroupHom.id G).completion = NormedAddGroupHom.id (Completion G)

Proof state:
G : Type u_1
inst✝ : SeminormedAddCommGroup G
⊢ (id G).completion = id (Completion G)

Tactic:
ext x

Result:
case H
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ (id G).completion x = (id (Completion G)) x

Proof state:
case H
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ (id G).completion x = (id (Completion G)) x

Tactic:
rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]

Result:
case H
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ _root_.id x = (id (Completion G)) x

Proof state:
case H
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ _root_.id x = (id (Completion G)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesAt.congr (hf : HasFPowerSeriesAt f p x) (hg : f =ᶠ[𝓝 x] g) :
    HasFPowerSeriesAt g p x

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
r₂ : ℝ≥0∞
h₂pos : r₂ > 0
h₂ : EMetric.ball x r₂ ⊆ {x | (fun x => f x = g x) x}
⊢ HasFPowerSeriesAt g p x

Tactic:
exact ⟨min r₁ r₂,
  (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr
    fun y hy => h₂ (EMetric.ball_subset_ball inf_le_right hy)⟩

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
⊢ HasFPowerSeriesAt g p x

Tactic:
rcases EMetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
r₂ : ℝ≥0∞
h₂pos : r₂ > 0
h₂ : EMetric.ball x r₂ ⊆ {x | (fun x => f x = g x) x}
⊢ HasFPowerSeriesAt g p x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
hg : f =ᶠ[𝓝 x] g
⊢ HasFPowerSeriesAt g p x

Tactic:
rcases hf with ⟨r₁, h₁⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
⊢ HasFPowerSeriesAt g p x
-- Mathlib/Data/Nat/Init.lean
lemma mul_self_inj : m * m = n * n ↔ m = n

Proof state:
m n : ℕ
⊢ m * m = n * n ↔ m = n

Tactic:
simp [Nat.le_antisymm_iff, mul_self_le_mul_self_iff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_smul (w : InfinitePlace K) (x : mixedSpace K) (c : ℝ) :
    normAtPlace w (c • x) = |c| * normAtPlace w x

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) =
    |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (normAtPlace w) (c • x) = |c| * (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) =
    |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
-- Mathlib/Order/Interval/Set/OrdConnected.lean
@[simp]
lemma image_subtype_val_Ico {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.val '' Ico x y = Ico x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ico (by simpa) x y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x => x ∈ s)).OrdConnected

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Vector α n) {H₁ H₂}
    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Vector α n
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : α), a ∈ l → q a
h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f l H₁ = pmap g l H₂

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toArray := l, size_toArray := ⋯ } H₁ = pmap g { toArray := l, size_toArray := ⋯ } H₂

Proof state:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ Array.pmap f l ⋯ = Array.pmap g l ⋯

Tactic:
apply Array.pmap_congr_left

Result:
case mk.h
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂

Proof state:
case mk.h
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toArray := l, size_toArray := ⋯ } H₁ = pmap g { toArray := l, size_toArray := ⋯ } H₂

Tactic:
simp only [pmap_mk, eq_mk]

Result:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
h : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ Array.pmap f l ⋯ = Array.pmap g l ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_toArray : v = List.toArray a ↔ v.toList = a

Proof state:
α✝ : Type u_1
v : Array α✝
a : List α✝
⊢ v = a.toArray ↔ v.toList = a

Tactic:
cases v

Result:
case mk
α✝ : Type u_1
a toList✝ : List α✝
⊢ { toList := toList✝ } = a.toArray ↔ { toList := toList✝ }.toList = a

Proof state:
case mk
α✝ : Type u_1
a toList✝ : List α✝
⊢ { toList := toList✝ } = a.toArray ↔ { toList := toList✝ }.toList = a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem disjoint_ndinsert_left {a : α} {s t : Multiset α} :
    Disjoint (ndinsert a s) t ↔ a ∉ t ∧ Disjoint s t :=
  Iff.trans (by simp [disjoint_left]) disjoint_cons_left

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint (ndinsert a s) t ↔ _root_.Disjoint (a ::ₘ s) t

Tactic:
simp [disjoint_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Subalgebra.rank_bot : Module.rank F (⊥ : Subalgebra F E) = 1 :=
  (Subalgebra.toSubmoduleEquiv (⊥ : Subalgebra F E)).symm.rank_eq.trans <| by
    rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]
    letI := Module.nontrivial F E
    exact LinearIndepOn.id_singleton _ one_ne_zero

Proof state:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ LinearIndepOn F id {1}

Tactic:
letI := Module.nontrivial F E

Result:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndepOn F id {1}

Proof state:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndepOn F id {1}

Tactic:
exact LinearIndepOn.id_singleton _ one_ne_zero

Result:
no goals

Proof state:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F ↥(toSubmodule ⊥) = 1

Tactic:
rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]

Result:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ LinearIndepOn F id {1}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem?_eraseIdx (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) :
    (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : List α
h : i < { toList := l }.size
⊢ ({ toList := l }.eraseIdx i h)[j]? = if j < i then { toList := l }[j]? else { toList := l }[j + 1]?

Tactic:
simp [List.getElem?_eraseIdx]

Result:
no goals

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
⊢ (l.eraseIdx i h)[j]? = if j < i then l[j]? else l[j + 1]?

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
l : List α
h : i < { toList := l }.size
⊢ ({ toList := l }.eraseIdx i h)[j]? = if j < i then { toList := l }[j]? else { toList := l }[j + 1]?
-- Mathlib/Algebra/GeomSum.lean
theorem mul_neg_geom_sum [Ring α] (x : α) (n : ℕ) : ((1 - x) * ∑ i ∈ range n, x ^ i) = 1 - x ^ n :=
  op_injective <| by simpa using geom_sum_mul_neg (op x) n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)

Tactic:
simpa using geom_sum_mul_neg (op x) n

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_zero : W.ΨSq 0 = 0

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 0 = 0

Tactic:
rw [← Nat.cast_zero, ΨSq_ofNat, preΨ'_zero, zero_pow two_ne_zero, zero_mul]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
lemma norm_sq_eq {x : E} : ‖x‖ ^ 2 = ‖⟪x, x⟫‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
⊢ ‖x‖ ^ 2 = ‖inner x x‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂,c₃] = 4

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Module.rank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]

Result:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ ↑4 = 4

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ ↑4 = 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_surjective_eq_zero_iff_lift :
    #{f : α → β' | Surjective f} = 0 ↔ lift.{v} #α < lift.{u} #β' ∨ (#α ≠ 0 ∧ #β' = 0)

Proof state:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ ¬#β' = 0) ∧ Nonempty (β' ↪ α)

Tactic:
simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
  Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]

Result:
no goals

Proof state:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} = 0 ↔ lift.{v, u} #α < lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0

Tactic:
rw [← not_iff_not, not_or, not_lt, lift_mk_le', ← Ne, not_and_or, not_ne_iff, and_comm]

Result:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ ¬#β' = 0) ∧ Nonempty (β' ↪ α)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem not_as_aig : ∀ (b : Bool), (true && !b) = !b

Proof state:
⊢ ∀ (b : Bool), (true && !b) = !b

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_mulSingle_of_ne (h : b ≠ 1) : mulSupport (mulSingle a b) = {a} :=
  mulSupport_mulSingle_subset.antisymm fun x (hx : x = a) => by
    rwa [mem_mulSupport, hx, mulSingle_eq_same]

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b : B
h : b ≠ 1
x : A
hx : x = a
⊢ x ∈ mulSupport (mulSingle a b)

Tactic:
rwa [mem_mulSupport, hx, mulSingle_eq_same]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_1728_of_two_eq_zero (h2 : (2 : F) = 0) : ofJ 1728 = ofJ0 F

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ ofJ 1728 = ofJ0 F

Tactic:
rw [ofJ, if_pos (by linear_combination 864 * h2),
  if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ 3 = 1

Tactic:
linear_combination h2

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ 1728 = 0

Tactic:
linear_combination 864 * h2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_self {x : BitVec w} : x ||| x = x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| x).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x ||| x = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| x).getLsbD i = x.getLsbD i
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The Dirichlet character mod `1` corresponds to the constant function `1`. -/
lemma modOne_eq_one {R : Type*} [CommSemiring R] {χ : DirichletCharacter R 1} :
    ((χ ·) : ℕ → R) = 1

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
χ : DirichletCharacter R 1
x✝ : ℕ
⊢ χ ↑x✝ = 1 x✝

Tactic:
rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
χ : DirichletCharacter R 1
⊢ (fun x => χ ↑x) = 1

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
χ : DirichletCharacter R 1
x✝ : ℕ
⊢ χ ↑x✝ = 1 x✝