mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
k : ℕ
h✝ : Finite α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact card_sym_eq_multichoose _ _

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Finsupp

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
⊢ ↑f.support.sym2 = map ⇑f ⁻¹' Function.support mul

Tactic:
by ext ⟨a, b⟩; simp

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l) <*>
      traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))

Tactic:
hr,

Goal state after:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r) =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r = pure (node (f v) (map f l) (map f r))

Tactic:
hr,

Goal state after:
case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r) = pure (node (f v) (map f l) (map f r))
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ node <$> (fun {α} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r

Tactic:
hr,

Goal state after:
case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ node <$> (fun {α} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : BinaryTree α
⊢ (fun {α} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t

Tactic:
by
  induction t with
  | nil => rw [traverse, traverse, η.preserves_pure]
  | node v l r hl hr =>
    rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Sum.Interval

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

Tactic:
rcases a with a | a <;> rcases b with b | b

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

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

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

case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ c ∈ sumLift₂ f g (inr a) (inr b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr
α₁ : 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 : γ₁ ⊕ γ₂
⊢ ((∃ 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₂) →
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b

Tactic:
rintro (⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ |
      ⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩)

Goal state after:
case mpr.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 γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b)

case mpr.inr.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 γ₂
a : α₁
b : β₂
c : γ₁
hc : c ∈ g₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

case mpr.inr.inr.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 γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

case mpr.inr.inr.inr
α₁ : 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
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)
Module: Mathlib.Dynamics.FixedPoints.Prufer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s

Tactic:
← smul_inv_smul g s

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| g • g⁻¹ • s
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ ((⇑(f a) ⁻¹' s) ∆ K) + μ (K ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2

Tactic:
symmDiff_of_ge ha.subset_preimage,

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ (⇑(f a) ⁻¹' s \ K) + μ (K ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : Dense (range fun x ↦ x • a)
⊢ False

Tactic:
← DenseRange,

Goal state after:
case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : DenseRange fun x ↦ x • a
⊢ False
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ ↑n.natAbs ^ j ∣ n ^ j

Tactic:
Int.natCast_natAbs,

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ |n| ^ j ∣ n ^ j
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ AEMeasurable (fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
· exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
x : X
x_s : x ∈ s
⊢ ∃ z ∈ t, z ∈ ball x (dynEntourage T U n)

Tactic:
simpa using! ht (hs.1 x_s)

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : IsEmpty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M →[L] N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
g : M →[L] N
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h : { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M ↪[L] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = (fun f ↦ f.toFun) g
⊢ { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M ≃[L] N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
g : M ≃[L] N
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
h₂ : { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun = g.invFun
⊢ { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
a : Language.empty.Structure M
⊢ a = default

Tactic:
by
    ext _ f <;> exact Empty.elim f

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case inl
α : Type u_1
fst✝ : ℕ
f : ring.Functions fst✝
⊢ Sum.inl ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
cases f

Goal state after:
case inl.add
α : Type u_1
⊢ Sum.inl ⟨2, add⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.mul
α : Type u_1
⊢ Sum.inl ⟨2, mul⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.neg
α : Type u_1
⊢ Sum.inl ⟨1, neg⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.zero
α : Type u_1
⊢ Sum.inl ⟨0, zero⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.one
α : Type u_1
⊢ Sum.inl ⟨0, one⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case inr
α : Type u_1
fst✝ : ℕ
f : ring.Relations fst✝
⊢ Sum.inr ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
cases f

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f✝ : R ≃+* S
n : ℕ
f : ring.Functions n
⊢ ∀ (x : Fin n → R), f✝.toFun (funMap f x) = funMap f (f✝.toFun ∘ x)

Tactic:
cases f

Goal state after:
case add
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap add x) = funMap add (f.toFun ∘ x)

case mul
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap mul x) = funMap mul (f.toFun ∘ x)

case neg
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 1 → R), f.toFun (funMap neg x) = funMap neg (f.toFun ∘ x)

case zero
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap zero x) = funMap zero (f.toFun ∘ x)

case one
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap one x) = funMap one (f.toFun ∘ x)
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f✝ : R ≃+* S
n : ℕ
f : ring.Relations n
⊢ ∀ (x : Fin n → R), RelMap f (f✝.toFun ∘ x) ↔ RelMap f x

Tactic:
cases f

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: case func
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
l✝ : ℕ
f : ring.Functions l✝
a : Fin l✝ → ring.Term α
ih : ∀ (a_1 : Fin l✝), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func f a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func f a))

Tactic:
cases f

Goal state after:
case func.add
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.add a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.add a))

case func.mul
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.mul a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.mul a))

case func.neg
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 1 → ring.Term α
ih : ∀ (a_1 : Fin 1), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.neg a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.neg a))

case func.zero
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.zero a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.zero a))

case func.one
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.one a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.one a))
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
cases f

Goal state after:
case func.zero.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions 0
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl

Goal state after: