harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Perfect.lean
theorem Perfect.closure_nhds_inter {U : Set α} (hC : Perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U)
    (Uop : IsOpen U) : Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty

Proof state:
case right
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ (closure (U ∩ C)).Nonempty

Tactic:
apply Nonempty.closure

Result:
case right.a
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ (U ∩ C).Nonempty

Proof state:
case left.hC
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ Preperfect (U ∩ C)

Tactic:
exact hC.acc.open_inter Uop

Result:
no goals

Proof state:
case right.a
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ (U ∩ C).Nonempty

Tactic:
exact ⟨x, ⟨xU, xC⟩⟩

Result:
no goals

Proof state:
case left
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ Perfect (closure (U ∩ C))

Tactic:
apply Preperfect.perfect_closure

Result:
case left.hC
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ Preperfect (U ∩ C)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ Perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).Nonempty

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ Perfect (closure (U ∩ C))

case right
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen U
⊢ (closure (U ∩ C)).Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈ l₁) :
    (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₁ l₂ : List α
h : ¬a ∈ l₁
⊢ (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b

Tactic:
simp [replace_append, h]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem isCoprime_group_smul_left : IsCoprime (x • y) z ↔ IsCoprime y z :=
  ⟨fun ⟨a, b, h⟩ => ⟨x • a, b, by rwa [smul_mul_assoc, ← mul_smul_comm]⟩, fun ⟨a, b, h⟩ =>
    ⟨x⁻¹ • a, b, by rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]⟩⟩

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1

Tactic:
rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]

Result:
no goals

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1

Tactic:
rwa [smul_mul_assoc, ← mul_smul_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lt_aleph0_iff_finite {α : Type u} : #α < ℵ₀ ↔ Finite α

Proof state:
α : Type u
⊢ #α < ℵ₀ ↔ Finite α

Tactic:
simp only [lt_aleph0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem true_eq_decide_iff {p : Prop} [h : Decidable p] : true = decide p ↔ p

Proof state:
p : Prop
h : Decidable p
⊢ true = decide p ↔ p

Tactic:
cases h with | _ q => simp [q]

Result:
no goals

Proof state:
case isTrue
p : Prop
q : p
⊢ true = decide p ↔ p

Tactic:
simp [q]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_sub_le (p q : R[X]) : degree (p - q) ≤ max (degree p) (degree q)

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).degree ≤ p.degree ⊔ q.degree

Tactic:
simpa only [degree_neg q] using degree_add_le p (-q)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
lemma σ_naturality_apply {n : ℕ} (i : Fin (n + 1)) (x : S _⦋n⦌) :
    f.app (op ⦋n + 1⦌) (S.σ i x) = T.σ i (f.app (op ⦋n⦌) x)

Proof state:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) x

Tactic:
exact congr_fun (SimplicialObject.σ_naturality f i) x

Result:
no goals

Proof state:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ f.app (op ⦋n + 1⦌) (SimplicialObject.σ S i x) = SimplicialObject.σ T i (f.app (op ⦋n⦌) x)

Tactic:
show (S.σ i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ T.σ i) x

Result:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) x
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem DifferentiableWithinAt.pow (ha : DifferentiableWithinAt 𝕜 a s x) :
    ∀ n : ℕ, DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x
  | 0 => by simp only [pow_zero, differentiableWithinAt_const]
  | n + 1 => by simp only [pow_succ', DifferentiableWithinAt.pow ha n, ha.mul]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableWithinAt 𝕜 a s x
⊢ DifferentiableWithinAt 𝕜 (fun x => a x ^ 0) s x

Tactic:
simp only [pow_zero, differentiableWithinAt_const]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableWithinAt 𝕜 a s x
n : ℕ
⊢ DifferentiableWithinAt 𝕜 (fun x => a x ^ (n + 1)) s x

Tactic:
simp only [pow_succ', DifferentiableWithinAt.pow ha n, ha.mul]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem disjoint_comap_iff_map {f : α → β} {F : Filter α} {G : Filter β} :
    Disjoint F (comap f G) ↔ Disjoint (map f F) G

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint F (comap f G) ↔ Disjoint (map f F) G

Tactic:
simp only [disjoint_iff, ← Filter.push_pull, map_eq_bot_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingularLift_addMap {P Q : PointClass F} (hP : W.NonsingularLift P)
    (hQ : W.NonsingularLift Q) : W.NonsingularLift <| W.addMap P Q

Proof state:
case mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Tactic:
rcases Q

Result:
case mk.mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Proof state:
case mk.mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Tactic:
exact nonsingular_add hP hQ

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
⊢ W.NonsingularLift (W.addMap P Q)

Tactic:
rcases P

Result:
case mk
F : Type u
inst✝ : Field F
W : Projective F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] lemma disjoint_primeFactors (ha : a ≠ 0) (hb : b ≠ 0) :
    Disjoint a.primeFactors b.primeFactors ↔ Coprime a b

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b

Tactic:
simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd, gcd_ne_zero_left,
  ha, hb]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded (f : G → E) {s : Set G}
    (hp : WithSeminorms p) :
    Bornology.IsVonNBounded 𝕜 (f '' s) ↔
      ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p (f x) < r

Proof state:
𝕜 : Type u_1
E : Type u_5
G : Type u_7
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r

Tactic:
simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem SurjOn.leftInvOn_of_rightInvOn (hf : SurjOn f s t) (hf' : RightInvOn f f' s) :
    LeftInvOn f f' t := fun y hy => by
  let ⟨x, hx, heq⟩ := hf hy
  rw [← heq, hf' hx]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f (f' y) = y

Tactic:
rw [← heq, hf' hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
⊢ f (f' y) = y

Tactic:
let ⟨x, hx, heq⟩ := hf hy

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f (f' y) = y
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem isPrefixOf_append {n m : Name} : ¬ n.hasMacroScopes → ¬ m.hasMacroScopes → n.isPrefixOf (n ++ m)

Proof state:
n m : Name
h1 : n.hasMacroScopes = false
h2 : m.hasMacroScopes = false
⊢ n.isPrefixOf (n.appendCore m) = true

Tactic:
clear h2

Result:
n m : Name
h1 : n.hasMacroScopes = false
⊢ n.isPrefixOf (n.appendCore m) = true

Proof state:
n m : Name
h1 : ¬n.hasMacroScopes = true
h2 : ¬m.hasMacroScopes = true
⊢ n.isPrefixOf (n ++ m) = true

Tactic:
show n.isPrefixOf (n.append m)

Result:
n m : Name
h1 : ¬n.hasMacroScopes = true
h2 : ¬m.hasMacroScopes = true
⊢ n.isPrefixOf (n.append m) = true

Proof state:
n m : Name
⊢ ¬n.hasMacroScopes = true → ¬m.hasMacroScopes = true → n.isPrefixOf (n ++ m) = true

Tactic:
intro h1 h2

Result:
n m : Name
h1 : ¬n.hasMacroScopes = true
h2 : ¬m.hasMacroScopes = true
⊢ n.isPrefixOf (n ++ m) = true

Proof state:
n m : Name
h1 : ¬n.hasMacroScopes = true
h2 : ¬m.hasMacroScopes = true
⊢ n.isPrefixOf (n.append m) = true

Tactic:
simp_all [Name.append]

Result:
n m : Name
h1 : n.hasMacroScopes = false
h2 : m.hasMacroScopes = false
⊢ n.isPrefixOf (n.appendCore m) = true

Proof state:
n m : Name
h1 : n.hasMacroScopes = false
⊢ n.isPrefixOf (n.appendCore m) = true

Tactic:
induction m <;> simp [*, Name.appendCore, isPrefixOf]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem le_induced_generateFrom {α β} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β}
    (h : ∀ a : Set β, a ∈ b → IsOpen (f ⁻¹' a)) : t ≤ induced f (generateFrom b)

Proof state:
case h
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ ∀ s ∈ preimage f '' b, IsOpen s

Tactic:
simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]

Result:
case h
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ ∀ a ∈ b, IsOpen (f ⁻¹' a)

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)

Tactic:
rw [induced_generateFrom_eq]

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)

Proof state:
case h
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ ∀ a ∈ b, IsOpen (f ⁻¹' a)

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)

Tactic:
apply le_generateFrom

Result:
case h
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen (f ⁻¹' a)
⊢ ∀ s ∈ preimage f '' b, IsOpen s
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensorμ_natural_right (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) :
    (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ =
      tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂)

Tactic:
convert tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1 <;> simp

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_sum]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
haveI := Fintype.ofFinite β

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_coord_change_source :
    ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I.symm ⁻¹' f.target ∩ ↑(f.extend I).symm ⁻¹' f'.source ∩ range ↑I = ↑I.symm ⁻¹' (f.symm ≫ₕ f').source ∩ range ↑I

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ((f.extend I).symm ≫ f'.extend I).source = ↑I '' (f.symm ≫ₕ f').source

Tactic:
simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source,
  extend_target, inter_right_comm _ (range I)]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I.symm ⁻¹' f.target ∩ ↑(f.extend I).symm ⁻¹' f'.source ∩ range ↑I = ↑I.symm ⁻¹' (f.symm ≫ₕ f').source ∩ range ↑I
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_eq_of_L1 (x : PiLp 1 β) : ‖x‖₊ = ∑ i : ι, ‖x i‖₊ :=
  NNReal.eq <| by push_cast; exact norm_eq_of_L1 x

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ x_1 : ι, ‖x x_1‖

Tactic:
exact norm_eq_of_L1 x

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ↑‖x‖₊ = ↑(∑ i : ι, ‖x i‖₊)

Tactic:
push_cast

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ x_1 : ι, ‖x x_1‖
-- Mathlib/Algebra/Order/Field/Power.lean
theorem Even.zpow_nonneg (hn : Even n) (a : α) : 0 ≤ a ^ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
simp [em']

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)

Tactic:
rw [zpow_add' (by simp [em'])]

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k
-- Mathlib/Order/OrderIsoNat.lean
theorem WellFounded.monotone_chain_condition [PartialOrder α] :
    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (IsWellFounded α fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
exact wellFoundedGT_iff_monotone_chain_condition

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
rw [← isWellFounded_iff]

Result:
α : Type u_1
inst✝ : PartialOrder α
⊢ (IsWellFounded α fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem alternatingWord_succ' (i i' : B) (m : ℕ) :
    alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m

Proof state:
B : Type u_1
i i' : B
m : ℕ
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m

Tactic:
induction' m with m ih generalizing i i'

Result:
case zero
B : Type u_1
i i' : B
⊢ alternatingWord i i' (0 + 1) = (if Even 0 then i' else i) :: alternatingWord i i' 0

case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ alternatingWord i i' (m + 1 + 1) = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Proof state:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
nth_rw 1 [ih i' i]

Result:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Proof state:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
rw [alternatingWord]

Result:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: (alternatingWord i' i m).concat i'

Proof state:
case zero
B : Type u_1
i i' : B
⊢ alternatingWord i i' (0 + 1) = (if Even 0 then i' else i) :: alternatingWord i i' 0

Tactic:
simp [alternatingWord]

Result:
no goals

Proof state:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: (alternatingWord i' i m).concat i'

Tactic:
simp [Nat.even_add_one, ← Nat.not_even_iff_odd]

Result:
no goals

Proof state:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ alternatingWord i i' (m + 1 + 1) = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
rw [alternatingWord]

Result:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
-- Mathlib/Algebra/IsPrimePow.lean
theorem IsPrimePow.pow {n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) :=
  let ⟨p, k', hp, hk', hn⟩ := hn
  ⟨p, k * k', hp, mul_pos hk.bot_lt hk', by rw [pow_mul', hn]⟩

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k

Tactic:
rw [pow_mul', hn]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_restrict_of_subset (h : s ⊆ t) : (μ.restrict t).restrict s = μ.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ (μ.restrict t).restrict s = μ.restrict s

Tactic:
ext1 u hu

Result:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict s) u

Proof state:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict s) u

Tactic:
rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]

Result:
case h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t

Proof state:
case h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t

Tactic:
exact inter_subset_right.trans h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKey? k' =
      if k == k' then
        if (f (m.get? k)).isSome then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKey? k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'

Tactic:
simp_to_model [alter] using List.getKey?_alterKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
    (a.set i v h)[i]'(by simp [h]) = v

Proof state:
α : Type ?u.471532
a : Array α
i : Nat
v : α
h : i < a.size
⊢ i < (a.set i v h).size

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
h : i < a.size
⊢ (a.set i v h)[i] = v

Tactic:
simp only [set, ← getElem_toList, List.getElem_set_self]

Result:
no goals