harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ZMod/Basic.lean
theorem RingHom.ext_zmod {n : ℕ} {R : Type*} [Semiring R] (f g : ZMod n →+* R) : f = g

Proof state:
case a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
a : ZMod n
⊢ f a = g a

Tactic:
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a

Result:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
⊢ f ↑k = g ↑k

Proof state:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k

Tactic:
show φ k = ψ k

Result:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ φ k = ψ k

Proof state:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k

Tactic:
let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))

Result:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k

Proof state:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
⊢ f ↑k = g ↑k

Tactic:
let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))

Result:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k

Proof state:
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ φ k = ψ k

Tactic:
rw [φ.ext_int ψ]

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
⊢ f = g

Tactic:
ext a

Result:
case a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
a : ZMod n
⊢ f a = g a
-- Mathlib/Data/List/Sublists.lean
theorem sublists'Aux_eq_map (a : α) (r₁ : List (List α)) : ∀ (r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁ :=
  List.reverseRecOn r₁ (fun _ => by simp [sublists'Aux]) fun r₁ l ih r₂ => by
    rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
    simp [sublists'Aux]

Proof state:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])

Tactic:
rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]

Result:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
    sublists'Aux a r₁ r₂ ++ [a :: l]

Proof state:
α : Type u
a : α
r₁ x✝ : List (List α)
⊢ sublists'Aux a [] x✝ = x✝ ++ map (cons a) []

Tactic:
simp [sublists'Aux]

Result:
no goals

Proof state:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
    sublists'Aux a r₁ r₂ ++ [a :: l]

Tactic:
simp [sublists'Aux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
    (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i

Proof state:
case mk
α : Type u_1
i : Nat
toList✝ : List α
⊢ ({ toList := toList✝ }.eraseIdxIfInBounds i).toList = { toList := toList✝ }.toList.eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
⊢ (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i

Tactic:
induction as

Result:
case mk
α : Type u_1
i : Nat
toList✝ : List α
⊢ ({ toList := toList✝ }.eraseIdxIfInBounds i).toList = { toList := toList✝ }.toList.eraseIdx i
-- Mathlib/Order/Disjoint.lean
theorem Disjoint.le_of_codisjoint (hab : Disjoint a b) (hbc : Codisjoint b c) : a ≤ c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c

Tactic:
rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
exact inf_le_inf_right _ le_sup_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
    (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i)

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ i < w → r ≤ i → x.getLsbD (i - r) = true → x.getLsbD (w - r + i) = true

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ ((x <<< r).getLsbD i || x.getLsbD (w - r + i)) = x.getLsbD (w - r + i)

Tactic:
simp

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ i < w → r ≤ i → x.getLsbD (i - r) = true → x.getLsbD (w - r + i) = true

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i)

Tactic:
rw [rotateLeftAux, getLsbD_or, getLsbD_ushiftRight]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ ((x <<< r).getLsbD i || x.getLsbD (w - r + i)) = x.getLsbD (w - r + i)
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.mem_closure_iff_exists_inseparable {K : Set X} (hK : IsCompact K) :
    y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
⊢ y ∉ closure K

Tactic:
have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
  (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
this : Disjoint (𝓝 y) (𝓝ˢ K)
⊢ y ∉ closure K

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure K
⊢ ∃ x ∈ K, Inseparable x y

Tactic:
contrapose! hy

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
⊢ y ∉ closure K

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
  (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure K
⊢ ∃ x ∈ K, Inseparable x y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
this : Disjoint (𝓝 y) (𝓝ˢ K)
⊢ y ∉ closure K

Tactic:
simpa only [disjoint_iff, not_mem_closure_iff_nhdsWithin_eq_bot]
  using this.mono_right principal_le_nhdsSet

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_isBase_iff : (freeOn E).IsBase B ↔ B = E

Proof state:
α : Type u_1
E B : Set α
⊢ (freeOn E).IsBase B ↔ B = E

Tactic:
simp only [freeOn, loopyOn_ground, dual_isBase_iff', loopyOn_isBase_iff, diff_eq_empty,
  ← subset_antisymm_iff, eq_comm (a := E)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_two {x : BitVec w} : x * 2#w = x + x

Proof state:
w : Nat
x : BitVec w
this : 2#w = 1#w + 1#w
⊢ x * 2#w = x + x

Tactic:
simp [this, mul_succ]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 2#w = 1#w + 1#w

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
⊢ (2#w).toNat = (1#w + 1#w).toNat

Proof state:
w : Nat
x : BitVec w
⊢ x * 2#w = x + x

Tactic:
have : 2#w = 1#w + 1#w := by apply BitVec.eq_of_toNat_eq; simp

Result:
w : Nat
x : BitVec w
this : 2#w = 1#w + 1#w
⊢ x * 2#w = x + x

Proof state:
case a
w : Nat
x : BitVec w
⊢ (2#w).toNat = (1#w + 1#w).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm_sub_le {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (hp : 1 ≤ p) : eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp : 1 ≤ p
⊢ eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
simpa [LpAddConst_of_one_le hp] using eLpNorm_sub_le' hf hg p

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig}
    {f : (aig : AIG α) → Ref aig → Entrypoint α} [LawfulOperator α Ref f] [LawfulMapOperator α f]
    {h} :
    ⟦f (f aig input1).aig (input2.cast h), assign⟧
      =
    ⟦f aig input2, assign⟧

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
assign : α → Bool
aig : AIG α
input1 input2 : aig.Ref
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : aig.decls.size ≤ (f aig input1).aig.decls.size
⊢ ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧

Tactic:
rw [LawfulMapOperator.chainable]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem coe_dualBasis : ⇑b.dualBasis = b.coord

Proof state:
case h.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i : ι
x : M
⊢ (b.dualBasis i) x = (b.coord i) x

Tactic:
apply dualBasis_apply

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ ⇑b.dualBasis = b.coord

Tactic:
ext i x

Result:
case h.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i : ι
x : M
⊢ (b.dualBasis i) x = (b.coord i) x
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem dist_comm (x y : Completion α) : dist x y = dist y x

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x

Tactic:
refine induction_on₂ x y ?_ ?_

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.1 x.2 = dist x.2 x.1}

case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist ↑a ↑b = dist ↑b ↑a

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist ↑a ↑b = dist ↑b ↑a

Tactic:
rw [Completion.dist_eq, Completion.dist_eq, dist_comm]

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist ↑a ↑b = dist ↑b ↑a

Tactic:
intro a b

Result:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist ↑a ↑b = dist ↑b ↑a

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.1 x.2 = dist x.2 x.1}

Tactic:
exact isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
    (Completion.continuous_dist continuous_snd continuous_fst)

Result:
no goals
-- Mathlib/GroupTheory/FiniteAbelian/Duality.lean
private
lemma dvd_exponent {ι G : Type*} [Finite ι] [CommGroup G] {n : ι → ℕ}
    (e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))) (i : ι) :
    n i ∣ Monoid.exponent G

Proof state:
ι : Type u_1
G : Type u_2
inst✝¹ : Finite ι
inst✝ : CommGroup G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i ∣ Monoid.exponent G

Tactic:
have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
  simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
    using (ZMod.addOrderOf_one (n i)).symm

Result:
ι : Type u_1
G : Type u_2
inst✝¹ : Finite ι
inst✝ : CommGroup G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
this : n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))
⊢ n i ∣ Monoid.exponent G

Proof state:
ι : Type u_1
G : Type u_2
inst✝¹ : Finite ι
inst✝ : CommGroup G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i ∣ Monoid.exponent G

Tactic:
classical have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
  simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
    using (ZMod.addOrderOf_one (n i)).symm
exact this ▸ Monoid.order_dvd_exponent _

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_2
inst✝¹ : Finite ι
inst✝ : CommGroup G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
this : n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))
⊢ n i ∣ Monoid.exponent G

Tactic:
exact this ▸ Monoid.order_dvd_exponent _

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_2
inst✝¹ : Finite ι
inst✝ : CommGroup G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))

Tactic:
simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
  using (ZMod.addOrderOf_one (n i)).symm

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isCoatomic_dual_iff_isAtomic [OrderBot α] : IsCoatomic αᵒᵈ ↔ IsAtomic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_top_or_exists_le_coatom⟩, fun h =>
    ⟨fun b => by apply h.eq_bot_or_exists_atom_le⟩⟩

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomic αᵒᵈ
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
apply h.eq_top_or_exists_le_coatom

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
@[simp] lemma invert_comp_C : invert ∘ (@C R _) = C

Proof state:
case h.h
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝) a✝ = (C x✝) a✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
⊢ ⇑invert ∘ ⇑C = ⇑C

Tactic:
ext

Result:
case h.h
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝) a✝ = (C x✝) a✝
-- Mathlib/GroupTheory/Exponent.lean
theorem Group.exponent_dvd_iff_forall_zpow_eq_one :
    (Monoid.exponent G : ℤ) ∣ n ↔ ∀ g : G, g ^ n = 1

Proof state:
G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.comp_inter_of_eq {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F}
    (x : E) (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (hy : f x = y) :
    ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
exact hg.comp_inter x hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atBot (hff' : ∀ᶠ x in atBot, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in atBot, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in atBot, g' x ≠ 0)
    (hfbot : Tendsto f atBot (𝓝 0)) (hgbot : Tendsto g atBot (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) atBot l) : Tendsto (fun x => f x / g x) atBot l

Proof state:
case intro.intro.intro.intro.intro.intro.intro
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atBot l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atBot
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atBot
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≤ l, b ∈ s
hl' : Iio l ⊆ s
⊢ Tendsto (fun x => f x / g x) atBot l✝

Tactic:
refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx => hg' x <| (hl' hx).2) hfbot hgbot hdiv <;>
  intro x hx <;> apply_assumption <;> first | exact (hl' hx).1.1| exact (hl' hx).1.2

Result:
no goals

Proof state:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atBot, ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩

Result:
case intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atBot, ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) atBot l

Proof state:
case intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ atBot, ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) atBot l

Tactic:
rcases hgg' with ⟨s₂, hs₂, hgg'⟩

Result:
case intro.intro.intro.intro
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v ∈ atBot, ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : s₁ ∈ atBot
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atBot
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
⊢ Tendsto (fun x => f x / g x) atBot l
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_dvd_iff {a : α} : s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Tactic:
apply Iff.trans Multiset.lcm_dvd

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Tactic:
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_eq_sum_range' [Algebra R S] {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    aeval x p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range n, (algebraMap R S) (p.coeff x_1) * x ^ x_1

Tactic:
exact eval₂_eq_sum_range' (algebraMap R S) hn x

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ i ∈ range n, p.coeff i • x ^ i

Tactic:
simp_rw [Algebra.smul_def]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range n, (algebraMap R S) (p.coeff x_1) * x ^ x_1
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_map_le (k : ℕ) : (derivedSeries R L' k).map f ≤ derivedSeries R L k

Proof state:
case succ
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeriesOfIdeal R L' k ⊤) ≤ derivedSeriesOfIdeal R L k ⊤
⊢ map f ⁅derivedSeriesOfIdeal R L' k ⊤, derivedSeriesOfIdeal R L' k ⊤⁆ ≤
    ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆

Tactic:
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ map f (derivedSeries R L' k) ≤ derivedSeries R L k

Tactic:
induction k with
| zero => simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]
| succ k ih =>
  simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
  exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
⊢ map f (derivedSeries R L' 0) ≤ derivedSeries R L 0

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_zero, le_top]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeries R L' k) ≤ derivedSeries R L k
⊢ map f (derivedSeries R L' (k + 1)) ≤ derivedSeries R L (k + 1)

Tactic:
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢

Result:
case succ
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : map f (derivedSeriesOfIdeal R L' k ⊤) ≤ derivedSeriesOfIdeal R L k ⊤
⊢ map f ⁅derivedSeriesOfIdeal R L' k ⊤, derivedSeriesOfIdeal R L' k ⊤⁆ ≤
    ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem and_any_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
    (q && l.any p) = l.any fun a => q && p a

Proof state:
α : Type u_1
l : List α
p : α → Bool
q : Bool
⊢ (q && l.any p) = l.any fun a => q && p a

Tactic:
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_left, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
q : Bool
head✝ : α
tail✝ : List α
ih : (q && tail✝.any p) = tail✝.any fun a => q && p a
⊢ (q && (p head✝ || tail✝.any p)) = (q && p head✝ || tail✝.any fun a => q && p a)

Tactic:
rw [Bool.and_or_distrib_left, ih]

Result:
no goals