mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), c ∈ Ioo (⋯ ▸ a) (⋯ ▸ b)) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
mem_Ioo,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a < c ∧ c < ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c < b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases e : Seq.destruct S with - | a <;> rw [e] at h'
    · exact
        let ⟨d, o, ad⟩ := IH _ _ h'
        let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
        ⟨c, Or.inl cl, ac⟩
    · obtain ⟨o, S'⟩ := a
      obtain - | c := o <;> simp only at h' <;> rcases IH _ _ h' with ⟨d, dl | dS', ad⟩
      · exact
          let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
          ⟨c, Or.inl cl, ac⟩
      · refine ⟨d, Or.inr ?_, ad⟩
        rw [Seq.destruct_eq_cons e]
        exact Seq.mem_cons_of_mem _ dS'
      · simp only [List.mem_cons] at dl
        rcases dl with dc | dl
        · rw [dc] at ad
          refine ⟨c, Or.inr ?_, ad⟩
          rw [Seq.destruct_eq_cons e]
          apply Seq.mem_cons
        · exact
            let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
            ⟨c, Or.inl cl, ac⟩
      · refine ⟨d, Or.inr ?_, ad⟩
        rw [Seq.destruct_eq_cons e]
        exact Seq.mem_cons_of_mem _ dS'

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case left
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)},
    a ∈ S.join.destruct →
      ∃ b ∈ T.join.destruct,
        LiftRelO R
          (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
          a b

Tactic:
intro
          apply liftRel_join.lem _ ST fun _ _ => id

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right.ST
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ swap (LiftRel (LiftRel R)) ?m.340 S

Tactic:
apply ST

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = (replicate n val).snoc val

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)

Tactic:
rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ ⨆ g', (f₂ g'⁻¹) ((f₁ g') x) + 1 = (⨆ g', (f₂ g'⁻¹) ((f₁ g') x)) + 1

Tactic:
exact (Monotone.map_ciSup_of_continuousAt (by fun_prop)
      (monotone_id.add_const (1 : ℝ)) (this x)).symm

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
induction n with

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
⊢ μ.rnDeriv ν x = μ'.rnDeriv ν x →
    (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x →
      μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
hx₂

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x →
    μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
mem_ball_symmetry

Goal state after:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this✝ : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν'
this : rnDeriv 0 ν' =ᵐ[ν'] 0
⊢ rnDeriv 0 ν' =ᵐ[ν.restrict h.nullSet] 0

Tactic:
by
    have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'
    exact h_ac'.ae_le this

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

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n = ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

pp: case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
· exact h' ▸ le_top

Goal state after:
case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

pp: case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
· exact h' ▸ le_top

Goal state after:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ netEntropyEntourage T ∅ U = ⊥

Tactic:
by
  rw [netEntropyEntourage, ← expGrowthSup_zero]
  congr
  simp only [netMaxcard_empty, ENat.toENNReal_zero, Pi.zero_def]

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

Goal state before:
pp: case inl
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n = ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

pp: case inr
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
· exact h' ▸ le_top

Goal state after:
case inr
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
rw [coverEntropy_eq_iSup_netEntropyEntourage T F]
  apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'
  refine iSup₂_le fun U U_uni ↦ ?_
  obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
  apply (netEntropyEntourage_antitone T F si_U).trans _
  exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyEntourage T F (s i)) i h_i

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ (sum fun x ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
rw [sum_const, lift_aleph0]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
exact gal_X_pow_sub_one_isSolvable n

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

Goal state before:
pp: ⊢ ring.card = 5

Tactic:
by
  have : Fintype.card Language.ring.Symbols = 5 := rfl
  simp [Language.card, this]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
⊢ M ↪ₑ[L[[↑A]]] f.toEmbedding.withConstants A

Tactic:
refine ⟨f, ?_⟩
  intro n φ x
  have h :
    (Sum.elim (fun a ↦ ↑(L.con a)) (⇑f ∘ x) :
      ↑A ⊕ Fin n → f.toEmbedding.withConstants A) =
    f ∘ Sum.elim (fun a ↦ ↑(L.con a)) x :=
    (Sum.comp_elim _ _ _).symm
  simpa only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv, h] using!
    f.map_formula
      (BoundedFormula.constantsVarsEquiv φ)
      (Sum.elim (fun a ↦ ↑(L.con a)) x)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs

Tactic:
induction n with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
⊢ φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs

Tactic:
induction n with

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toHom.range = ⊤

Tactic:
ext n

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ n ∈ f.toHom.range ↔ n ∈ ⊤
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ

Tactic:
· intro h
    obtain ⟨v, hv⟩ := (Formula.realize_exClosure φ).1 h
    let v' := fun a => if hmem : a ∈ φ.freeVarFinset
      then v ⟨a, hmem⟩ else Classical.choice inferInstance
    exists v'
    refine (Formula.realize_equivSentence_symm M (Formula.equivSentence φ) v').mp ?_
    simpa [Equiv.symm_apply_apply, Formula.Realize] using
      (BoundedFormula.realize_restrictFreeVar v' (by grind)).1 hv

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
have : Inhabited h'.some := Classical.inhabited_of_nonempty'

Goal state after:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
this : Inhabited ↑(Nonempty.some h')
⊢ (φ.onTheory T).IsSatisfiable
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default ⇑xs.some

Tactic:
· rintro _ i j ij rfl
    simpa using ij

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m

Tactic:
refine ⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩
  rintro ⟨k, hk⟩
  have : ↑m < ℵ₀ := natCast_lt_aleph0
  rw [hk, mul_lt_aleph0_iff] at this
  rcases this with (h | h | ⟨-, hk'⟩)
  iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk; simp [hk]
  lift k to ℕ using hk'
  exact ⟨k, mod_cast hk⟩

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
n : ℕ
a : R
⊢ logDeriv (a ^ n) = ↑n * logDeriv a

Tactic:
induction n with

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
· simp only [expand_X, map_mul]
    intro _ _ hf; rw [hf, frobenius_def]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
a : K
p : MvPolynomial σ K
⊢ (fun e ↦ (eval e) (a • p)) = (RingHom.id K) a • fun e ↦ (eval e) p

Tactic:
by ext e; simp

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n, e n • indicator n) = e

Tactic:
ext n

Goal state after:
case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ (evalₗ K σ) (∑ n, e n • indicator n) n = e n
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ (fun x ↦ (algebraMap K L) (a x)) = fun x ↦ 0

Tactic:
RingHom.map_det,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : ((MvPolynomial.eval (⇑(algebraMap K L) ∘ b)).mapMatrix M).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ (fun x ↦ (algebraMap K L) (a x)) = fun x ↦ 0
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) * Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) * (Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z))

Tactic:
by
            apply congr_arg (Quot.mk _)
            simp only [mul_assoc, iterate_map_mul, ← iterate_add_apply,
              add_comm, add_left_comm]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
⊢ mk K p (n, 0) = 0

Tactic:
induction n with

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
⊢ x = 0

Tactic:
by_cases hn : n = 0
    · rwa [hn, pow_zero, pow_one] at h
    rw [hp, zero_pow hn, pow_zero] at h
    subsingleton [subsingleton_of_zero_eq_one h.symm]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1] ((⇑(frobenius K p))^[y.1 + z2] z.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
rw [← iterate_add_apply]

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1 + (y.1 + z2)] z.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
⊢ mk K p x ^ n = mk K p (x.1, x.2 ^ n)

Tactic:
induction n with

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n x : ℕ
⊢ ↑x = mk K p (n, ↑x)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (f ≫ g)) a = (Hom.hom g) ((Hom.hom f) a)

Tactic:
simp only [hom_comp, ContinuousMonoidHom.comp_toFun]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R ↥B
x : ↥B
⊢ (Algebra.leftMulMatrix (H.basisOfBasisRight H' b)) ((algebraMap (↥B) S) x) =
    (algebraMap R ↥A).mapMatrix ((Algebra.leftMulMatrix b) x)

Tactic:
by
  ext
  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H']

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ carrier 0 = {0}

Tactic:
by
  ext; rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h.h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝¹ x✝ : L
⊢ (mk K x✝¹).minpoly = (mk K x✝).minpoly ↔ mk K x✝¹ = mk K x✝

Tactic:
simp [isConjRoot_def]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]

Goal state after: