harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem ext_rat_on_pnat (same_on_neg_one : f (-1) = g (-1))
    (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_rat' <|
    DFunLike.congr_fun <|
      show
        (f : ℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤ →*₀ ℚ) =
          (g : ℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤ →*₀ ℚ)
        from ext_int' (by simpa) (by simpa)

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ (n : ℕ), 0 < n → ((↑f).comp ↑(Int.castRingHom ℚ)) ↑n = ((↑g).comp ↑(Int.castRingHom ℚ)) ↑n

Tactic:
simpa

Result:
no goals

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ((↑f).comp ↑(Int.castRingHom ℚ)) (-1) = ((↑g).comp ↑(Int.castRingHom ℚ)) (-1)

Tactic:
simpa

Result:
no goals
-- Mathlib/Control/LawfulFix.lean
theorem ωScottContinuous_toUnitMono (f : Part α → Part α) (hc : ωScottContinuous f) :
    ωScottContinuous (toUnitMono ⟨f,hc.monotone⟩) := .of_map_ωSup_of_orderHom fun _ => by
  ext ⟨⟩ : 1
  dsimp [OmegaCompletePartialOrder.ωSup]
  erw [hc.map_ωSup, Chain.map_comp]; rfl

Proof state:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (ωSup x✝) PUnit.unit =
    ωSup (x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })) PUnit.unit

Tactic:
dsimp [OmegaCompletePartialOrder.ωSup]

Result:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ f (Part.ωSup (x✝.map (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))

Proof state:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (ωSup x✝) = ωSup (x✝.map (toUnitMono { toFun := f, monotone' := ⋯ }))

Tactic:
ext ⟨⟩ : 1

Result:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ (toUnitMono { toFun := f, monotone' := ⋯ }) (ωSup x✝) PUnit.unit =
    ωSup (x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })) PUnit.unit

Proof state:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ f (Part.ωSup (x✝.map (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))

Tactic:
erw [hc.map_ωSup, Chain.map_comp]

Result:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (x✝.map ({ toFun := f, monotone' := ⋯ }.comp (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (x✝.map ({ toFun := f, monotone' := ⋯ }.comp (Pi.evalOrderHom PUnit.unit)))

Proof state:
case h.unit
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (x✝.map ({ toFun := f, monotone' := ⋯ }.comp (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (x✝.map ({ toFun := f, monotone' := ⋯ }.comp (Pi.evalOrderHom PUnit.unit)))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff_add_ncard (s t : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ (s \ t).ncard + t.ncard = (s ∪ t).ncard

Tactic:
rw [← ncard_union_eq disjoint_sdiff_left hs.diff ht, diff_union_self]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioc : (some : α → WithTop α) ⁻¹' Ioc a b = Ioc a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csInf_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddBelow s) : sInf s ∈ s

Proof state:
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ sInf s ∈ s

Tactic:
convert (leastOfBdd _ (Classical.choose_spec h2) h1).2.1

Result:
case h.e'_5
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ sInf s = ↑((Classical.choose h2).leastOfBdd ⋯ h1)

s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ DecidablePred (Membership.mem s)

Proof state:
case h.e'_5
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ sInf s = ↑((Classical.choose h2).leastOfBdd ⋯ h1)

s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ DecidablePred (Membership.mem s)

Tactic:
exact dif_pos ⟨h1, h2⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem SeminormedGroup.tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
    TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ i in l, ∀ x ∈ s, ‖f i x‖ < ε

Proof state:
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

Tactic:
simp only [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findFinIdx?_toList (p : α → Bool) (v : Vector α n) :
    v.toList.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast v.size_toArray.symm)

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ List.findFinIdx? p v.toList = Option.map (Fin.cast ⋯) (findFinIdx? p v)

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
v : Array α
⊢ List.findFinIdx? p { toArray := v, size_toArray := ⋯ }.toList =
    Option.map (Fin.cast ⋯) (findFinIdx? p { toArray := v, size_toArray := ⋯ })

Proof state:
case mk
α : Type u_1
p : α → Bool
v : Array α
⊢ List.findFinIdx? p { toArray := v, size_toArray := ⋯ }.toList =
    Option.map (Fin.cast ⋯) (findFinIdx? p { toArray := v, size_toArray := ⋯ })

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanIso.mul_eq_mul (hf : IsMulFreimanIso 2 A B f) {a b c d : α}
    (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) :
    f a * f b = f c * f d ↔ a * b = c * d

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ f a * f b = f c * f d ↔ a * b = c * d

Tactic:
simp_rw [← prod_pair]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ {f a, f b}.prod = {f c, f d}.prod ↔ {a, b}.prod = {c, d}.prod

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ {f a, f b}.prod = {f c, f d}.prod ↔ {a, b}.prod = {c, d}.prod

Tactic:
refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) <;> simp [ha, hb, hc, hd]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
theorem nonarchimedean_of_emb (f : G →* H) (emb : IsOpenEmbedding f) : NonarchimedeanGroup H :=
  { is_nonarchimedean := fun U hU =>
      have h₁ : f ⁻¹' U ∈ 𝓝 (1 : G)

Proof state:
case a
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ U ∈ 𝓝 (f 1)

Tactic:
rwa [f.map_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ ⇑f ⁻¹' U ∈ 𝓝 1

Tactic:
apply emb.continuous.tendsto

Result:
case a
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ U ∈ 𝓝 (f 1)
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem zero_base {n : ℕ} : maxPowDiv 0 n = 0

Proof state:
n : ℕ
⊢ maxPowDiv 0 n = 0

Tactic:
dsimp [maxPowDiv]

Result:
n : ℕ
⊢ go 0 0 n = 0

Proof state:
n : ℕ
⊢ go 0 0 n = 0

Tactic:
rw [maxPowDiv.go]

Result:
n : ℕ
⊢ (if 1 < 0 ∧ 0 < n ∧ n % 0 = 0 then go (0 + 1) 0 (n / 0) else 0) = 0

Proof state:
n : ℕ
⊢ (if 1 < 0 ∧ 0 < n ∧ n % 0 = 0 then go (0 + 1) 0 (n / 0) else 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natAbs_ediv (a b : ℤ) (H : b ∣ a) : natAbs (a / b) = natAbs a / natAbs b

Proof state:
case inl
a b : ℤ
H : b ∣ a
h : b.natAbs = 0
⊢ (a / 0).natAbs = a.natAbs / natAbs 0

Tactic:
simp [Int.ediv_zero]

Result:
no goals

Proof state:
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs * 1 = (a / b).natAbs * (b.natAbs / b.natAbs)

Tactic:
rw [Nat.div_self h]

Result:
no goals

Proof state:
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs * b.natAbs / b.natAbs = (a / b * b).natAbs / b.natAbs

Tactic:
rw [natAbs_mul (a / b) b]

Result:
no goals

Proof state:
case inl
a b : ℤ
H : b ∣ a
h : b.natAbs = 0
⊢ (a / b).natAbs = a.natAbs / b.natAbs

Tactic:
rw [natAbs_eq_zero.1 h]

Result:
case inl
a b : ℤ
H : b ∣ a
h : b.natAbs = 0
⊢ (a / 0).natAbs = a.natAbs / natAbs 0

Proof state:
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b * b).natAbs / b.natAbs = a.natAbs / b.natAbs

Tactic:
rw [Int.ediv_mul_cancel H]

Result:
no goals

Proof state:
case inr
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs = a.natAbs / b.natAbs

Tactic:
calc
  natAbs (a / b) = natAbs (a / b) * 1 := by rw [Nat.mul_one]
  _ = natAbs (a / b) * (natAbs b / natAbs b) := by rw [Nat.div_self h]
  _ = natAbs (a / b) * natAbs b / natAbs b := by rw [Nat.mul_div_assoc _ b.natAbs.dvd_refl]
  _ = natAbs (a / b * b) / natAbs b := by rw [natAbs_mul (a / b) b]
  _ = natAbs a / natAbs b := by rw [Int.ediv_mul_cancel H]

Result:
no goals

Proof state:
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs = (a / b).natAbs * 1

Tactic:
rw [Nat.mul_one]

Result:
no goals

Proof state:
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs * (b.natAbs / b.natAbs) = (a / b).natAbs * b.natAbs / b.natAbs

Tactic:
rw [Nat.mul_div_assoc _ b.natAbs.dvd_refl]

Result:
no goals

Proof state:
a b : ℤ
H : b ∣ a
⊢ (a / b).natAbs = a.natAbs / b.natAbs

Tactic:
rcases Nat.eq_zero_or_pos (natAbs b) with (h | h)

Result:
case inl
a b : ℤ
H : b ∣ a
h : b.natAbs = 0
⊢ (a / b).natAbs = a.natAbs / b.natAbs

case inr
a b : ℤ
H : b ∣ a
h : b.natAbs > 0
⊢ (a / b).natAbs = a.natAbs / b.natAbs
-- Mathlib/RingTheory/Frobenius.lean
lemma mul_inv_mem_inertia (H : IsArithFrobAt R σ Q) (H' : IsArithFrobAt R σ' Q) :
    σ * σ'⁻¹ ∈ Q.toAddSubgroup.inertia G

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
⊢ σ * σ'⁻¹ ∈ (Submodule.toAddSubgroup Q).inertia G

Tactic:
intro x

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
x : S
⊢ (σ * σ'⁻¹) • x - x ∈ Submodule.toAddSubgroup Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
x : S
⊢ (σ * σ'⁻¹) • x - x ∈ Submodule.toAddSubgroup Q

Tactic:
simpa [mul_smul] using sub_mem (H (σ'⁻¹ • x)) (H' (σ'⁻¹ • x))

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem strictAntiOn_deriv (hfc : StrictConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
    StrictAntiOn (deriv f) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictAntiOn (deriv f) S

Tactic:
simpa only [Pi.neg_def, deriv.neg, neg_neg] using
  (hfc.neg.strictMonoOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_lt_sub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b

Proof state:
a b c : ℕ
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries_add {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) :
    LSeries (f + g) s = LSeries f s + LSeries g s

Proof state:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f + g) s = LSeries f s + LSeries g s

Tactic:
simpa [LSeries, term_add] using tsum_add hf hg

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc_map [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) :
    trunc S n (map σ f p) = MvPolynomial.map f (trunc R n p)

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
⊢ (trunc S n) ((map σ f) p) = (MvPolynomial.map f) ((trunc R n) p)

Tactic:
ext m

Result:
case a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc S n) ((map σ f) p)) = MvPolynomial.coeff m ((MvPolynomial.map f) ((trunc R n) p))

Proof state:
case a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc S n) ((map σ f) p)) = MvPolynomial.coeff m ((MvPolynomial.map f) ((trunc R n) p))

Tactic:
simp [coeff_trunc, MvPolynomial.coeff_map, apply_ite f]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem mem_ordConnectedComponent_comm :
    y ∈ ordConnectedComponent s x ↔ x ∈ ordConnectedComponent s y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y

Tactic:
rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem Chain.backwards_induction (p : α → Prop) (l : List α) (h : Chain r a l)
    (hb : getLast (a :: l) (cons_ne_nil _ _) = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
    (final : p b) : ∀ i ∈ a :: l, p i

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (i : α), i ∈ (a :: l).reverse → p i

Tactic:
apply this.induction _ _ (fun _ _ h ↦ carries h)

Result:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (lne : (a :: l).reverse ≠ []), p ((a :: l).reverse.head lne)

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (i : α), i ∈ a :: l → p i

Tactic:
simp_rw (config := {singlePass := true}) [← List.mem_reverse]

Result:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (i : α), i ∈ (a :: l).reverse → p i

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ Chain' (flip (flip r)) (a :: l)

Tactic:
simpa [Chain']

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ ∀ (i : α), i ∈ a :: l → p i

Tactic:
have : Chain' (flip (flip r)) (a :: l) := by simpa [Chain']

Result:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip (flip r)) (a :: l)
⊢ ∀ (i : α), i ∈ a :: l → p i

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (lne : (a :: l).reverse ≠ []), p ((a :: l).reverse.head lne)

Tactic:
simpa only [ne_eq, reverse_eq_nil_iff, not_false_eq_true, head_reverse, forall_true_left, hb,
  reduceCtorEq]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip (flip r)) (a :: l)
⊢ ∀ (i : α), i ∈ a :: l → p i

Tactic:
replace this := chain'_reverse.mpr this

Result:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : Chain r a l
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
this : Chain' (flip r) (a :: l).reverse
⊢ ∀ (i : α), i ∈ a :: l → p i
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_eq_zero_iff {x : 𝕜} : (x : AddCircle p) = 0 ↔ ∃ n : ℤ, n • p = x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p x : 𝕜
⊢ ↑x = 0 ↔ ∃ n, n • p = x

Tactic:
simp [AddSubgroup.mem_zmultiples_iff]

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
private lemma auxDFT_neg (Φ : ZMod N → E) : auxDFT (fun j ↦ Φ (-j)) = fun k ↦ auxDFT Φ (-k)

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ ZMod.auxDFT (fun j => Φ (-j)) k = ZMod.auxDFT Φ (-k)

Tactic:
simpa only [auxDFT] using
Fintype.sum_equiv (Equiv.neg _) _ _ (fun j ↦ by rw [Equiv.neg_apply, neg_mul_neg])

Result:
no goals

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ (ZMod.auxDFT fun j => Φ (-j)) = fun k => ZMod.auxDFT Φ (-k)

Tactic:
ext1 k

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ ZMod.auxDFT (fun j => Φ (-j)) k = ZMod.auxDFT Φ (-k)

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
⊢ stdAddChar (-(j * k)) • Φ (-j) = stdAddChar (-((Equiv.neg (ZMod N)) j * -k)) • Φ ((Equiv.neg (ZMod N)) j)

Tactic:
rw [Equiv.neg_apply, neg_mul_neg]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem derivBFamily_lt_ord_lift {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c}
    (hc : IsRegular c) (hι : Cardinal.lift.{v, u} o.card < c) (hc' : c ≠ ℵ₀)
    (hf : ∀ (i hi), ∀ b < c.ord, f i hi b < c.ord) {a} :
    a < c.ord → derivBFamily.{u, v} o f a < c.ord :=
  derivFamily_lt_ord_lift hc (by rwa [mk_toType]) hc' fun _ => hf _ _

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord
a : Ordinal.{max u v}
⊢ lift.{?u.139031, u} #o.toType < c

Tactic:
rwa [mk_toType]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem map_comp (h1 : LEComap g B C) (h2 : LEComap f A B) :
    map (g.comp f) (h1.comp h2) = map g h1 ∘ map f h2

Proof state:
case h.mk
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (g.comp f) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2

Tactic:
ext ⟨⟩

Result:
case h.mk
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (g.comp f) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid) a✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
    (x * y).getLsbD i = (mulRec x y w).getLsbD i

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getLsbD i = (x * setWidth w (setWidth (w + 1) y)).getLsbD i

Tactic:
rw [setWidth_setWidth_of_le]

Result:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getLsbD i = (x * setWidth w y).getLsbD i

case h
w : Nat
x y : BitVec w
i : Nat
⊢ w ≤ w + 1

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getLsbD i = (x * setWidth w y).getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getLsbD i = (x.mulRec y w).getLsbD i

Tactic:
simp only [mulRec_eq_mul_signExtend_setWidth]

Result:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getLsbD i = (x * setWidth w (setWidth (w + 1) y)).getLsbD i

Proof state:
case h
w : Nat
x y : BitVec w
i : Nat
⊢ w ≤ w + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_bot_right (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) : map₂ f p ⊥ = ⊥ :=
  eq_bot_iff.2 <|
    map₂_le.2 fun m _hm n hn => by
      rw [Submodule.mem_bot] at hn
      rw [hn, LinearMap.map_zero]; simp only [mem_bot]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥

Tactic:
simp only [mem_bot]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n ∈ ⊥
⊢ (f m) n ∈ ⊥

Tactic:
rw [Submodule.mem_bot] at hn

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) n ∈ ⊥

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) n ∈ ⊥

Tactic:
rw [hn, LinearMap.map_zero]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ 0 ∈ ⊥
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mem_idealLattice {x : mixedSpace K} :
    x ∈ idealLattice K I ↔ ∃ y, y ∈ (I : Set K) ∧ mixedEmbedding K y = x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ idealLattice K I ↔ ∃ y ∈ ↑↑I, (mixedEmbedding K) y = x

Tactic:
simp [idealLattice]

Result:
no goals