harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_eq_zero_iff_cos_eq {z : ℂ} : sin z = 0 ↔ cos z = 1 ∨ cos z = -1

Proof state:
z : ℂ
h : sin z = 0
⊢ 0 = sin z * sin z

Tactic:
rw [h, mul_zero]

Result:
no goals

Proof state:
z : ℂ
⊢ sin z = 0 ↔ 0 = sin z * sin z

Tactic:
exact ⟨fun h => by rw [h, mul_zero], eq_zero_of_mul_self_eq_zero ∘ Eq.symm⟩

Result:
no goals

Proof state:
z : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, ← sub_eq_iff_eq_add, sub_self]

Result:
z : ℂ
⊢ sin z = 0 ↔ 0 = sin z * sin z
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem one_rightUnitor {M : Mon_ C} :
    ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = M.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = M.one

Tactic:
simp [← unitors_equal]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma surjectivity [∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)]
    {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ]
    (hXκ : HasCardinalLT (Subobject X) κ) (z : X ⟶ c.pt) :
    ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this : IsFiltered J
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀

Tactic:
have := hc.mono_ι_app_of_isFiltered

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝ : IsFiltered J
this : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [inst : colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀
-- Mathlib/Order/Interval/Basic.lean
theorem coe_iInf [DecidableRel (α := α) (· ≤ ·)] (f : ι → Interval α) :
    ↑(⨅ i, f i) = ⋂ i, (f i : Set α)

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
f : ι → Interval α
⊢ ↑(⨅ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_mutuallySingular (s : SignedMeasure α) (μ : Measure α) :
    s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ
      s.toJordanDecomposition.negPart.singularPart μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hl :
  ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨
    ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rcases hl with hp | hn

Result:
case neg.inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hp : ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

case neg.inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
hn : ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_reciprocal (n : ℕ) :
    commProb (Product (reciprocalFactors n)) = 1 / n

Proof state:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
this : n / 2 < n
⊢ Odd 3

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Instances/Rat.lean
theorem totallyBounded_Icc (a b : ℚ) : TotallyBounded (Icc a b)

Proof state:
a b : ℚ
⊢ TotallyBounded (Icc a b)

Tactic:
simpa only [preimage_cast_Icc]
  using totallyBounded_preimage Rat.isUniformEmbedding_coe_real.isUniformInducing
    (totallyBounded_Icc (a : ℝ) b)

Result:
no goals
-- Mathlib/Order/Zorn.lean
theorem exists_maximal_of_chains_bounded (h : ∀ c, IsChain r c → ∃ ub, ∀ a ∈ c, a ≺ ub)
    (trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) : ∃ m, ∀ a, m ≺ a → a ≺ m :=
  have : ∃ ub, ∀ a ∈ maxChain r, a ≺ ub := h _ <| maxChain_spec.left
  let ⟨ub, (hub : ∀ a ∈ maxChain r, a ≺ ub)⟩ := this
  ⟨ub, fun a ha =>
    have : IsChain r (insert a <| maxChain r) :=
      maxChain_spec.1.insert fun b hb _ => Or.inr <| trans (hub b hb) ha
    hub a <| by
      rw [maxChain_spec.right this (subset_insert _ _)]
      exact mem_insert _ _⟩

Proof state:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
rw [maxChain_spec.right this (subset_insert _ _)]

Result:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)

Proof state:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)

Tactic:
exact mem_insert _ _

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1

Proof state:
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1

Tactic:
rw [mul_comm, mul_inv_of_unit a h]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem elim_update_left [DecidableEq α] [DecidableEq β] (f : α → γ) (g : β → γ) (i : α) (c : γ) :
    Sum.elim (Function.update f i c) g = Function.update (Sum.elim f g) (inl i) c

Proof state:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x

Tactic:
rcases x with x | x

Result:
case h.inl
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

case h.inr
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)

Proof state:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

Tactic:
subst h

Result:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)

Proof state:
case neg
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.inr
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)

Tactic:
simp

Result:
no goals

Proof state:
case h.inl
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

Tactic:
by_cases h : x = i

Result:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

case neg
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
⊢ Sum.elim (update f i c) g = update (Sum.elim f g) (inl i) c

Tactic:
ext x

Result:
case h
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x
-- Mathlib/Analysis/Convex/Jensen.lean
/-- Convex **strict Jensen inequality**.

If the function is strictly convex, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.

See also `StrictConvexOn.map_sum_eq_iff`. -/
lemma StrictConvexOn.map_sum_lt (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) :
    f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj✝ : j ∈ t
k : ι
hk✝ : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι
hj : j ∉ u
hk : k ∉ u
ht : t = cons j (cons k u hk) ⋯
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
subst ht

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this : k ∈ (cons j (cons k u hk✝) ⋯).erase j
⊢ f (∑ i ∈ cons j (cons k u hk✝) ⋯, w i • p i) < ∑ i ∈ cons j (cons k u hk✝) ⋯, w i • f (p i)
-- Mathlib/CategoryTheory/LiftingProperties/Limits.lean
lemma IsPushout.hasLiftingProperty (h : IsPushout s f g t)
    {Z' W' : C} (g' : Z' ⟶ W') [HasLiftingProperty f g'] : HasLiftingProperty g g' where
  sq_hasLift := fun {u v} sq ↦ by
    have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v

Tactic:
rw [h.inr_desc_assoc, CommSq.fac_right]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v

Tactic:
rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ sq.HasLift

Tactic:
exact ⟨h.desc u (CommSq.mk w).lift (by rw [CommSq.fac_left]), h.inl_desc ..,
  h.hom_ext (by rw [h.inl_desc_assoc, sq.w]) (by rw [h.inr_desc_assoc, CommSq.fac_right])⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ g ≫ h.desc u ⋯.lift ⋯ ≫ g' = g ≫ v

Tactic:
rw [h.inl_desc_assoc, sq.w]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ s ≫ u = f ≫ ⋯.lift

Tactic:
rw [CommSq.fac_left]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ sq.HasLift

Tactic:
have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v) := by
  rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ sq.HasLift
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α] [Inhabited α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k k' : α} (k_beq : k == k')
    (h : containsKey k l = false)
    (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
    getKey! k' (insertListIfNewUnit l toInsert) = k

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
h : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getKey! k' (insertListIfNewUnit l toInsert) = k

Tactic:
rw [getKey!_eq_getKey?,
  getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq h distinct mem, Option.get!_some]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem update_le_update_iff :
    Function.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
simp +contextual [update_le_iff]

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toEquiv_inclusion {f g : M ≃ₚ[L] N} (h : f ≤ g) :
    g.toEquiv.toEmbedding.comp (Substructure.inclusion (dom_le_dom h)) =
      (Substructure.inclusion (cod_le_cod h)).comp f.toEquiv.toEmbedding

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ g.toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp f.toEquiv.toEmbedding

Tactic:
rw [← (subtype _).comp_inj, subtype_toEquiv_inclusion h]

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x✝ : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝ = (g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)) x✝

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x✝ : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝ = (g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)) x✝
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem IsTransitive.powerset (h : x.IsTransitive) : (powerset x).IsTransitive :=
  fun y hy z hz => by
  rw [mem_powerset] at hy ⊢
  exact h.subset_of_mem (hy hz)

Proof state:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ⊆ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ⊆ x

Tactic:
exact h.subset_of_mem (hy hz)

Result:
no goals

Proof state:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ x.powerset
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x.powerset

Tactic:
rw [mem_powerset] at hy ⊢

Result:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ⊆ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ⊆ x
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (l : Filter α) :
    map₂ f l (pure b) = l

Proof state:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map₂ f l (pure b) = l

Tactic:
rw [map₂_pure_right, funext h, map_id']

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem accepts_reindex (g : σ ≃ σ') : (reindex g M).accepts = M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ x ∈ ((reindex g) M).accepts ↔ x ∈ M.accepts

Tactic:
simp [mem_accepts]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
⊢ ((reindex g) M).accepts = M.accepts

Tactic:
ext x

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ x ∈ ((reindex g) M).accepts ↔ x ∈ M.accepts
-- Mathlib/Data/Sum/Interval.lean
lemma mem_sumLexLift :
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
      (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
        (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
          (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
            ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Proof state:
case mp.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ (∃ a_1 ∈ f₁ a b, Embedding.inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case mp.inl.inl.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f₁ a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Proof state:
case mp.inl.inr.refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ a_1 ∈ g₁ a b, inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case mp.inl.inr.refine_1.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₁
hc : c ∈ g₁ a b
h : inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
-- Mathlib/Topology/MetricSpace/CantorScheme.lean
theorem map_mem (x : (inducedMap A).1) (n : ℕ) : (inducedMap A).2 x ∈ A (res x n)

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
have := x.property.some_mem

Result:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some ⋯ ∈ ⋂ n, A (res (↑x) n)
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some ⋯ ∈ A (res (↑x) i)
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
exact this n

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some ⋯ ∈ ⋂ n, A (res (↑x) n)
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
rw [mem_iInter] at this

Result:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some ⋯ ∈ A (res (↑x) i)
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)