mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
repeat rw [Kernel.deterministic_comp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
repeat rw [Kernel.deterministic_comp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun ω ↦ (f ω, g ω)) =
      μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) ↔
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
congr!

Goal state after:
case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun ω ↦ (f ω, g ω)) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ

case e'_3
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) =
    ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
repeat rw [Kernel.deterministic_comp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic
      (((((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.map id ⇑MeasurableEquiv.prodAssoc) ∘
              Prod.map id (Prod.map Prod.swap id)) ∘
            Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ∘
          ⇑MeasurableEquiv.prodAssoc) ∘
        Prod.map id Function.diag ∘ Prod.map Function.diag id)
      ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
⊢ Measure.map (fun a ↦ (k a, g a, f a)) μ =
    Measure.map (⇑e.symm) (Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ))

Tactic:
Measure.map_map (by fun_prop) (by fun_prop),

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
⊢ Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm ∘ ⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [integral_tilted_mul_eq_mgf, exp_sub]
    rwa [exp_cgf]

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm)
      (Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ))

Tactic:
Measure.map_map (by fun_prop) (by fun_prop),

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm ∘ ⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case mpr
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ (∃ a, 0 < a ∧ ↑a ≤ X ω) → 0 < X ω

Tactic:
intro ⟨q, h1, h2⟩
      exact lt_of_lt_of_le (q.cast_pos.2 h1) h2

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
hl : Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)
⊢ (κ ω').real {ω | ↑ε ≤ X ω} = 0

Tactic:
apply le_antisymm

Goal state after:
case a
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
hl : Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)
⊢ (κ ω').real {ω | ↑ε ≤ X ω} ≤ 0

case a
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
hl : Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)
⊢ 0 ≤ (κ ω').real {ω | ↑ε ≤ X ω}
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
inst✝³ : Semiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid W
inst✝ : Module A W
ρ : Representation A G W
toSubmodule✝ : Submodule A W
apply_mem_toSubmodule✝ : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule✝ → (ρ g) v ∈ toSubmodule✝
⊢ ∀ ⦃a₂ : Subrepresentation ρ⦄,
    { toSubmodule := toSubmodule✝, apply_mem_toSubmodule := apply_mem_toSubmodule✝ }.toSubmodule = a₂.toSubmodule →
      { toSubmodule := toSubmodule✝, apply_mem_toSubmodule := apply_mem_toSubmodule✝ } = a₂

Tactic:
congr!

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑n * ↑c))

Tactic:
have h := (sum_of_iIndepFun h_indep (c := fun _ ↦ c)
    (s := Finset.range n) (by simpa)).measure_ge_le hε

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
h : μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, c)))
⊢ μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑n * ↑c))
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
⊢ ∀ (x y : ρ.IntertwiningMap ρ),
    (equivLinearMapAsModule ρ ρ) (x * y) = (equivLinearMapAsModule ρ ρ) x * (equivLinearMapAsModule ρ ρ) y

Tactic:
intro f g

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f g : ρ.IntertwiningMap ρ
⊢ (equivLinearMapAsModule ρ ρ) (f * g) = (equivLinearMapAsModule ρ ρ) f * (equivLinearMapAsModule ρ ρ) g
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
g : G
⊢ X.ρ.invariants.subtype ∘ₗ (Representation.trivial k G ↑((invariantsFunctor k G).obj X)) g =
    X.ρ g ∘ₗ X.ρ.invariants.subtype

Tactic:
ext x; exact (x.2 g).symm

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x

Tactic:
have : x = 0 := Subsingleton.elim _ _

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
this : x = 0
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
hb : b ≠ ⟦g⟧
⊢ b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
induction b using Quotient.inductionOn with | h b =>
    have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb
    simp_all

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
x✝ : ↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A)
⊢ (Hom.hom ((coindResAdjunction k S).unit.app A)).toLinearMap x✝ =
    (Hom.hom ((indResAdjunction k S.subtype).unit.app A ≫ (resFunctor S.subtype).map A.indCoindIso.hom)).toLinearMap x✝

Tactic:
simp [coindResAdjunction]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X Y : Rep k H
f : X ⟶ Y
x✝² : H
x✝¹ : ↑A
x✝ : ↑X
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk X).compr₂
                  (ModuleCat.Hom.hom
                    (((coinvariantsTensor k H).obj (ind φ A)).map f ≫ (coinvariantsTensorIndIso φ A Y).hom)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk X).compr₂
                  (ModuleCat.Hom.hom
                    ((coinvariantsTensorIndIso φ A X).hom ≫ (resFunctor φ ⋙ (coinvariantsTensor k G).obj A).map f)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝

Tactic:
simp [coinvariantsTensorIndHom, coinvariantsTensorMk, hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x✝ : ↑A
⊢ x✝ ∈ A.ρ.invariants ↔ x✝ ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).ker

Tactic:
simpa [sub_hom, sub_eq_zero]
    using Representation.mem_invariants_iff_of_forall_mem_zpowers A.ρ g hg _

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

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
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
⊢ IsMulCoboundary₁ f

Tactic:
use (Units.mk0 (aux f z) hz)⁻¹

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
⊢ ∀ (g : Gal(L/K)), g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
refine ⟨a, ?_, ?_⟩

Goal state after:
case refine_1
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ a ≠ 0

case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f (g * h) = f g + f h

Tactic:
rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : ¬Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
simp [sub_hom, hj, Rep.applyAsHom, coinvariantsTensorMk, TensorProduct.tmul_sub,
        ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹, Module.End.mul_eq_comp]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X Y : Rep R G
φ : X ⟶ Y
⊢ tateComplex X ⟶ tateComplex Y

Tactic:
refine CochainComplex.ConnectData.map _ _ (chainsMap (.id G) φ) (cochainsMap (.id G) φ) ?_
  ext
  simp [Rep.tateNorm_eq, Representation.norm, Rep.hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯ = 1

Tactic:
ext; simp; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp (x✝¹ * x✝)) ⋯ ⋯ ⋯ =
    LaxMonoidalFunctor.isoOfComponents (equivApp x✝¹) ⋯ ⋯ ⋯ * LaxMonoidalFunctor.isoOfComponents (equivApp x✝) ⋯ ⋯ ⋯

Tactic:
ext; simp; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
⊢ η₁ = η₂

Tactic:
have := Fintype.ofFinite G
  classical
  ext X v
  have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
  have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
  rw [h, ← h2] at h1
  simpa using congr(($h1).hom (single 1 1))

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯

Tactic:
apply le_antisymm

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R ≤ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯

case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ≤ idealOfVars σ R