mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
this : ∀ (a_1 : Set α), ((fun x ↦ a + x) ∘ fun x ↦ -x) '' a_1 = (fun x ↦ a + x) '' (fun x ↦ -x) '' a_1
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ 1 • f = f

Tactic:
by simp only [← Filter.map_smul, one_smul, map_id']

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
← Filter.map_map

Goal state after:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1)) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ↑(⟨x, hx⟩ * ⟨y, hy⟩) = ↑(⟨y, hy⟩ * ⟨x, hx⟩)

Tactic:
refine eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy
        all_goals fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, ContinuousOn (f i) t) →
    ContinuousOn (fun a ↦ (Multiset.map (fun i ↦ f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) t

Tactic:
simpa using continuousOn_list_prod l

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (1 * 1))

Tactic:
refine .mul ?_ ?_

Goal state after:
case refine_1
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
⊢ (range (denseSeq G) ∩ (fun y ↦ x * y) ⁻¹' L).Nonempty

Tactic:
by
      rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
      exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y))
⊢ (fun n ↦ f n * g n) / g =ᶠ[l] f

Tactic:
exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
⊢ f x = g x

Tactic:
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)

Goal state after:
case inl
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x

case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by
  conv in _ * _ => rw [mul_comm]
  exact hg.mul_atTop' hf

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

Tactic:
by
  rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this : Finite ↑kl
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
have : Finite kr := k_fin.subset (by simp [k_eq])

Goal state after:
case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this✝ : Finite ↑kl
this : Finite ↑kr
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
let _ := Preorder.topology α

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
let _ := Preorder.topology α

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ = Preorder.topology α
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))

Tactic:
TopologicalSpace.tendsto_nhds_generateFrom_iff,

Goal state after:
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, f x ∈ s → f ⁻¹' s ∈ 𝓝[≤] x
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ Set.range (_root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
Set.range_comp,

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Set.range (Subtype.val ∘ ⇑(hom e.hom)) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Set.range (Subtype.val ∘ ⇑(hom e.hom)) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
Set.range_comp,

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.range ⇑(hom e.hom) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
⊢ ∀ (X : WalkingMulticospan J), F.obj X = G.obj X

Tactic:
rintro (_ | _)

Goal state after:
case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.obj (WalkingMulticospan.left a✝) = G.obj (WalkingMulticospan.left a✝)

case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ F.obj (WalkingMulticospan.right a✝) = G.obj (WalkingMulticospan.right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
⊢ ∀ (X : WalkingMulticospan J), (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app X = eqToHom ⋯

Tactic:
rintro (_ | _)

Goal state after:
case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.left a✝) = eqToHom ⋯

case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.right a✝) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
⊢ Function.Surjective (Sum.elim left right)

Tactic:
rintro (_ | _)

Goal state after:
case left
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.L
⊢ ∃ a, Sum.elim left right a = left a✝

case right
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.R
⊢ ∃ a, Sum.elim left right a = right a✝
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
LinearMap.exact_iff

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom S.g).ker = (ConcreteCategory.hom S.f).range
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u // J.fst l = r' }
T₂ : Type := { u // J.snd l = r' }
f : T₁ ⊕ T₂ → (left l ⟶ right r') :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ Function.Surjective f

Tactic:
rintro (_ | _)

Goal state after:
case left.right.fst
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.fst l }
T₂ : Type := { u // J.snd l = J.fst l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.fst l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.fst l

case left.right.snd
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.snd l }
T₂ : Type := { u // J.snd l = J.snd l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.snd l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.snd l
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
rintro (_ | _)

Goal state after:
case left
J : MultispanShape
a✝ : J.L
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (left a✝)) =
    left a✝

case right
J : MultispanShape
a✝ : J.R
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (right a✝)) =
    right a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
rintro (_ | _)

Goal state after:
case inl
J : MultispanShape
val✝ : J.L
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inl val✝)) =
    Sum.inl val✝

case inr
J : MultispanShape
val✝ : J.R
⊢ (fun x ↦
        match x with
        | left a => Sum.inl a
        | right b => Sum.inr b)
      (Sum.elim left right (Sum.inr val✝)) =
    Sum.inr val✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse
    (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))) fun f ↦
    match f.right, f.left, f.hom with
    | x, .(x), Hom.id .(x) => Sum.inl x
    | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
    | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a)

Tactic:
rintro ⟨_, _, (_ | _ | _)⟩ <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ (X : WalkingMulticospan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.L
⊢ (match WalkingMulticospan.left a✝, WalkingMulticospan.left a✝, 𝟙 (WalkingMulticospan.left a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.left a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
a✝ : J.R
⊢ (match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝, 𝟙 (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)
    | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
    | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a => I.left a
      | WalkingMulticospan.right b => I.right b)