harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma fwdDiff_smul {R : Type} [Ring R] [Module R G] (f : M → R) (g : M → G) :
    Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g

Proof state:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
y : M
⊢ f (y + h) • g (y + h) - f y • g y =
    f (y + h) • g y - f y • g y + (f y • g (y + h) - f y • g y) +
      (f (y + h) • g (y + h) - f y • g (y + h) - (f (y + h) • g y - f y • g y))

Tactic:
abel

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
⊢ Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g

Tactic:
ext y

Result:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
y : M
⊢ Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y

Proof state:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
y : M
⊢ Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y

Tactic:
simp only [fwdDiff, Pi.smul_apply', Pi.add_apply, smul_sub, sub_smul]

Result:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
y : M
⊢ f (y + h) • g (y + h) - f y • g y =
    f (y + h) • g y - f y • g y + (f y • g (y + h) - f y • g y) +
      (f (y + h) • g (y + h) - f y • g (y + h) - (f (y + h) • g y - f y • g y))
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem restrict (h : IsPartition π) (hJ : J ≤ I) : IsPartition (π.restrict J) :=
  isPartition_iff_iUnion_eq.2 <| by simp [h.iUnion_eq, hJ]

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : π.IsPartition
hJ : J ≤ I
⊢ (π.restrict J).iUnion = ↑J

Tactic:
simp [h.iUnion_eq, hJ]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem algebraicIndependent_iff_transcendental {x : A} :
    AlgebraicIndependent R ![x] ↔ Transcendental R x

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
⊢ AlgebraicIndependent R ![x] ↔ Transcendental R x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldr_subtype {p : α → Prop} {l : Vector { x // p x } n}
    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
    l.foldr f x = l.unattach.foldr g x

Proof state:
α : Type u_1
n : Nat
β : Type u_2
p : α → Prop
l : Vector { x // p x } n
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : Array { x // p x }
⊢ foldr f x { toArray := l, size_toArray := ⋯ } = foldr g x { toArray := l, size_toArray := ⋯ }.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : Array { x // p x }
⊢ foldr f x { toArray := l, size_toArray := ⋯ } = foldr g x { toArray := l, size_toArray := ⋯ }.unattach

Tactic:
simp [Array.foldr_subtype hf]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
lemma _root_.ModuleTopology.eq_coinduced_of_surjective
    {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
    moduleTopology R B = TopologicalSpace.coinduced φ inferInstance

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this : TopologicalSpace B := moduleTopology R B
⊢ moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance

Tactic:
haveI : IsModuleTopology R B := ⟨rfl⟩

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : TopologicalSpace B := moduleTopology R B
this : IsModuleTopology R B
⊢ moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : TopologicalSpace B := moduleTopology R B
this : IsModuleTopology R B
⊢ moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance

Tactic:
exact (isQuotientMap_of_surjective hφ).eq_coinduced

Result:
no goals

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
⊢ moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance

Tactic:
letI : TopologicalSpace B := moduleTopology R B

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this : TopologicalSpace B := moduleTopology R B
⊢ moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance
-- Mathlib/Analysis/Analytic/Basic.lean
theorem radius_smul_eq (p : FormalMultilinearSeries 𝕜 E F) {c : 𝕜} (hc : c ≠ 0) :
    (c • p).radius = p.radius

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
p : FormalMultilinearSeries 𝕜 E F
c : 𝕜
hc : c ≠ 0
⊢ (c • p).radius ≤ p.radius

Tactic:
exact radius_le_smul.trans_eq (congr_arg _ <| inv_smul_smul₀ hc p)

Result:
no goals

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
p : FormalMultilinearSeries 𝕜 E F
c : 𝕜
hc : c ≠ 0
⊢ (c • p).radius = p.radius

Tactic:
apply eq_of_le_of_le _ radius_le_smul

Result:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
c : 𝕜
hc : c ≠ 0
⊢ (c • p).radius ≤ p.radius
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.of_mul_right_left (H : IsRelPrime x (y * z)) : IsRelPrime x y

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime (y * z) x
⊢ IsRelPrime y x

Tactic:
exact H.of_mul_left_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at H ⊢

Result:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime (y * z) x
⊢ IsRelPrime y x
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_zero {x : PGame} : x ⧏ 0 ↔ ∃ j, ∀ i, (x.moveRight j).moveLeft i ⧏ 0

Proof state:
x : PGame
⊢ ((∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ moveLeft 0 i) ∧
          ∀ (j : (moveLeft 0 i).RightMoves), x ⧏ (moveLeft 0 i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0) ∧
          ∀ (j' : RightMoves 0), x.moveRight j ⧏ moveRight 0 j') ↔
    ∃ j, ∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0

Tactic:
simp

Result:
no goals

Proof state:
x : PGame
⊢ x ⧏ 0 ↔ ∃ j, ∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0

Tactic:
rw [lf_def]

Result:
x : PGame
⊢ ((∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ moveLeft 0 i) ∧
          ∀ (j : (moveLeft 0 i).RightMoves), x ⧏ (moveLeft 0 i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0) ∧
          ∀ (j' : RightMoves 0), x.moveRight j ⧏ moveRight 0 j') ↔
    ∃ j, ∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma limitsOfShape_monotone {W₁ W₂ : MorphismProperty C} (h : W₁ ≤ W₂)
    (J : Type*) [Category J] :
    W₁.limitsOfShape J ≤ W₂.limitsOfShape J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
⊢ W₁.limitsOfShape J ≤ W₂.limitsOfShape J

Tactic:
rintro _ _ _ ⟨_, _, _, _, h₁, _, f, hf⟩

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂✝ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W₁.functorCategory J f
⊢ W₂.limitsOfShape J (h₂✝.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{u_3, u_2} J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂✝ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W₁.functorCategory J f
⊢ W₂.limitsOfShape J (h₂✝.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Tactic:
exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic'_zero (R : Type*) [CommRing R] [IsDomain R] : cyclotomic' 0 R = 1

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 0 R = 1

Tactic:
simp only [cyclotomic', Finset.prod_empty, primitiveRoots_zero]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem eq_empty (x : ZFSet.{u}) : x = ∅ ↔ ∀ y : ZFSet.{u}, y ∉ x

Proof state:
x : ZFSet.{u}
⊢ x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

Tactic:
simp [ZFSet.ext_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addU_of_Z_eq_zero_right {P Q : Fin 3 → F} (hQz : Q z = 0) : addU P Q = 0

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0

Tactic:
rw [addU, hQz, mul_zero <| P z, div_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (α ⊕ γ)) (f : α ⊕ γ → β) :
    ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset (α ⊕ γ)
f : α ⊕ γ → β
⊢ ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)

Tactic:
rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disj_sum, Finset.toLeft_disjSum,
  Finset.toRight_disjSum]

Result:
no goals
-- Mathlib/RingTheory/DualNumber.lean
lemma fst_eq_zero_iff_eps_dvd [Semiring R] {x : R[ε]} :
    x.fst = 0 ↔ ε ∣ x

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 → ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
intro

Result:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
a✝ : TrivSqZeroExt.fst x = 0
⊢ ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
a✝ : TrivSqZeroExt.fst x = 0
⊢ ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
exact ⟨.inl x.snd, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ε ∣ x

Tactic:
simp_rw [dvd_def, TrivSqZeroExt.ext_iff, TrivSqZeroExt.fst_mul, TrivSqZeroExt.snd_mul,
  fst_eps, snd_eps, zero_mul, zero_smul, zero_add, MulOpposite.smul_eq_mul_unop,
  MulOpposite.unop_op, one_mul, exists_and_left, iff_self_and]

Result:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 → ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1
-- Mathlib/NumberTheory/SmoothNumbers.lean
theorem mul_mem_smoothNumbers {m₁ m₂ n : ℕ}
    (hm1 : m₁ ∈ n.smoothNumbers) (hm2 : m₂ ∈ n.smoothNumbers) : m₁ * m₂ ∈ n.smoothNumbers

Proof state:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ n.smoothNumbers
hm2 : m₂ ∈ n.smoothNumbers
⊢ m₁ * m₂ ∈ n.smoothNumbers

Tactic:
rw [smoothNumbers_eq_factoredNumbers] at hm1 hm2 ⊢

Result:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Proof state:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Tactic:
exact mul_mem_factoredNumbers hm1 hm2

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem minSqFac_prime {n d : ℕ} (h : n.minSqFac = some d) : Prime d

Proof state:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Tactic:
exact this.1

Result:
no goals

Proof state:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ Prime d

Tactic:
rw [h] at this

Result:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Proof state:
n d : ℕ
h : n.minSqFac = some d
⊢ Prime d

Tactic:
have := minSqFac_has_prop n

Result:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ Prime d
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem monic_scaleRoots_iff {p : R[X]} (s : R) : Monic (scaleRoots p s) ↔ Monic p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).Monic ↔ p.Monic

Tactic:
simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem mem_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) :
    J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
classical exact Finset.mem_union

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
exact Finset.mem_union

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_cpow_of_re_pos {p : ℂ × ℂ} (h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0) (h₂ : 0 < p.2.re) :
    ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) p

Proof state:
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)

case mk.inr
w : ℂ
h₂ : 0 < (0, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (0, w)

Tactic:
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]

Result:
no goals

Proof state:
p : ℂ × ℂ
h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0
h₂ : 0 < p.2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) p

Tactic:
obtain ⟨z, w⟩ := p

Result:
case mk
z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)

Proof state:
case mk
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)

Tactic:
rcases h₁ with (h₁ | (rfl : z = 0))

Result:
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)

case mk.inr
w : ℂ
h₂ : 0 < (0, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (0, w)

Proof state:
case mk
z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)

Tactic:
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
  not_le_zero_iff] at h₁

Result:
case mk
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (z, w)
-- Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
theorem tmul_zero_coe_mul_coe_tmul {i₂ : ι} (a₁ : A) (b₁ : ℬ 0) (a₂ : 𝒜 i₂) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) =
      ((a₁ * a₂ : A) ᵍ⊗ₜ (b₁ * b₂ : B))

Proof state:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem insert_mem_nhdsWithin_of_subset_insert [T1Space X] {x y : X} {s t : Set X}
    (hu : t ⊆ insert y s) : insert x s ∈ 𝓝[t] x

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x

Tactic:
refine nhdsWithin_mono x hu ?_

Result:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
⊢ insert x s ∈ 𝓝[t] x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Result:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s t : Set X
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x

Proof state:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s t : Set X
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x

Tactic:
exact mem_of_superset self_mem_nhdsWithin hu

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x

Tactic:
rw [nhdsWithin_insert_of_ne h]

Result:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x

Tactic:
exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_update_one [DecidableEq α] (f : α → M) (x : α) :
    mulSupport (update f x 1) = mulSupport f \ {x}

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x : α
⊢ mulSupport (update f x 1) = mulSupport f \ {x}

Tactic:
ext a

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x a : α
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : One M
inst✝ : DecidableEq α
f : α → M
x a : α
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
rcases eq_or_ne a x with rfl | hne <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
    x.rotateLeft (r % w) = x.rotateLeft r

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ x.rotateLeft (r % w) = x.rotateLeft r

Tactic:
simp only [rotateLeft, Nat.mod_mod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findRevM?_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
    v.toArray.findRevM? p = v.findRevM? p

Proof state:
case mk
m : Type → Type
α : Type
inst✝ : Monad m
p : α → m Bool
v : Array α
⊢ Array.findRevM? p { toArray := v, size_toArray := ⋯ }.toArray = findRevM? p { toArray := v, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type
α : Type
n : Nat
inst✝ : Monad m
p : α → m Bool
v : Vector α n
⊢ Array.findRevM? p v.toArray = findRevM? p v

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
m : Type → Type
α : Type
inst✝ : Monad m
p : α → m Bool
v : Array α
⊢ Array.findRevM? p { toArray := v, size_toArray := ⋯ }.toArray = findRevM? p { toArray := v, size_toArray := ⋯ }
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_comp_apply (hg : MDifferentiableAt I' I'' g (f x))
    (hf : MDifferentiableAt I I' f x) (v : TangentSpace I x) :
    mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
⊢ (mfderiv I I'' (g ∘ f) x) v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)

Tactic:
rw [mfderiv_comp _ hg hf]

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
⊢ ((mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)) v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
⊢ ((mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)) v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)

Tactic:
rfl

Result:
no goals