mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ ∃ H, N.IsComplement' H

Tactic:
replace hH : Nat.card (H.map K.subtype) = N.index := by
    rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ g ∉ (φ i).range

Tactic:
rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1

Tactic:
intro h
    simp only [pow_one, xa_sq] at h
    injection h with h'
    apply_fun ZMod.val at h'
    apply_fun (· / n) at h'
    simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self,
      Nat.div_self (NeZero.pos n), reduceCtorEq] at h'

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    ⟨k, hk⟩ ∈ MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)

Tactic:
simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_map_kleinFour_ofSubtype hs,
    Subgroup.mk_smul, MulAut.smul_def, MulAut.inv_apply, MulAut.conj_symm_apply, Subgroup.coe_mul,
    Subgroup.coe_inv, ← ConjAct.toConjAct_inv_smul, Equiv.Perm.support_toConjAct_eq_smul_support,
    mem_map_kleinFour_ofSubtype (s := g • s) (by simpa), Finset.subset_smul_finset_iff,
    ConjAct.toConjAct_smul, cycleType_conj, mul_inv_eq_one, mul_eq_left]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case of
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ ((of i) g • w).prod = (of i) g * w.prod

Tactic:
rw [of_smul_eq_smul, prod_summand_smul]

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (Kernel.piecewise hs κ η)

Tactic:
by
  refine ⟨fun a => ⟨?_⟩⟩
  rw [piecewise_apply', measure_univ, measure_univ, ite_self]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ κ)

Tactic:
simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, comp_sum_left, comp_sum_right]
  infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : α), (κ b) s ∂(deterministic g hg) a = (κ (g a)) s

Tactic:
deterministic_apply hg a,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : α), (κ b) s ∂Measure.dirac (g a) = (κ (g a)) s
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((deterministic f mf ×ₖ κ) a) s = (κ a) (Prod.mk (f a) ⁻¹' s)

Tactic:
rw [prod_apply' _ _ _ hs, lintegral_deterministic']
  exact measurable_measure_prodMk_left hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ μ ⟂ₘ ν

Tactic:
rw [← withDensity_rnDeriv_eq_zero]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = μ

Tactic:
by
  simp [hf]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable (fun x ↦ (∫ (a : α), rexp (f a) ∂μ)⁻¹ • rexp (f x) • g x) μ

Tactic:
congr! 2 with a

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
⊢ (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = (∫ (a : α), rexp (f a) ∂μ)⁻¹ • rexp (f a) • g a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_8
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : α) ∂(Kernel.const Unit μ) (), Integrable (fun y ↦ f (x, y)) ((prodMkLeft Unit κ) ((), x))) ∧
      Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂(prodMkLeft Unit κ) ((), x)) ((Kernel.const Unit μ) ()) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

Tactic:
Kernel.prodMkLeft_apply,

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_8
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ (∀ᵐ (x : α) ∂(Kernel.const Unit μ) (), Integrable (fun y ↦ f (x, y)) (κ x)) ∧
      Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) ((Kernel.const Unit μ) ()) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y ↦ f (x, y)) (κ x)) ∧ Integrable (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: case inr.inr
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬↑↑f =ᵐ[μ] 0
h'p : p < ∞
hp : p ≠ 0
⊢ Nontrivial ↥(Lp ℝ p μ)

Tactic:
have h'f : AEFinStronglyMeasurable f μ :=
      MemLp.aefinStronglyMeasurable (Lp.memLp f) hp h'p.ne

Goal state after:
case inr.inr
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬↑↑f =ᵐ[μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑↑f) μ
⊢ Nontrivial ↥(Lp ℝ p μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    ↑c * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ

Tactic:
simp only [integral_smul_nnreal_measure, measureReal_nnreal_smul_apply]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ c • ∫ (a : α), llr (c • μ) ν a ∂μ + ν.real univ - ↑c * μ.real univ =
    ↑c * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg.h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ μ ≪ c • ν

Tactic:
exact hμν.smul_right (by simpa)

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ ¬μ ≪ c • ν

Tactic:
refine fun h_contra ↦ hμν ?_
      rw [hν_smul]
      exact h_contra.smul_right (by simpa)

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
rw [klDiv_ne_top_iff]

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ↑‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_

Goal state after:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
⊢ s.shift c r = map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑p)))) s

Tactic:
by
  have h : Nonempty s := ⟨p⟩
  simp only [shift, h, ↓reduceDIte]
  ext q
  simp only [mem_map, AffineEquiv.coe_toAffineMap, AffineEquiv.constVAdd_apply]
  constructor <;> intro ⟨x, hx, heq⟩ <;> rw [← heq]
  · refine ⟨(1 - r) • (p.val -ᵥ h.some.val) +ᵥ x, ?_, ?_⟩
    · exact vadd_mem_of_mem_direction (smul_mem _ _ (vsub_mem_direction p.prop h.some.prop)) hx
    · rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]
  · refine ⟨(1 - r) • (h.some.val -ᵥ p.val) +ᵥ x, ?_, ?_⟩
    · exact vadd_mem_of_mem_direction (smul_mem _ _ (vsub_mem_direction h.some.prop p.prop)) hx
    · rw [vadd_vadd, ← smul_add, vsub_add_vsub_cancel]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((basis b ibc).repr ((b.repr v) i • ε (b i))) i = (algebraMap R S) ((b.repr v) i)

Tactic:
rw [← IsScalarTower.algebraMap_smul S (b.repr v i) (ε (b i)),
      map_smul, ← ibc.basis_apply]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((algebraMap R S) ((b.repr v) i) • (basis b ibc).repr ((basis b ibc) i)) i = (algebraMap R S) ((b.repr v) i)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ ∃ q ∈ affineSpan k (p '' {i}ᶜ), w i • (p i -ᵥ p j) +ᵥ q = (affineCombination k univ p) w

Tactic:
refine ⟨-(w i • (p i -ᵥ p j)) +ᵥ affineCombination k univ p w, ?_, by simp⟩

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ -(w i • (p i -ᵥ p j)) +ᵥ (affineCombination k univ p) w ∈ affineSpan k (p '' {i}ᶜ)
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : i = j
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
← hij,

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : i = j
⊢ f (b i) = (b.coord i) (f (b i)) • b i
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
hpure_tensor :
  ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
⊢ (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).compl₂ (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
        TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) +
      (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).flip.compl₂
          (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
        TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) =
    LinearMap.compr₂ (QuadraticMap.polarBilin (QuadraticForm.baseChange A Q))
      (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q))

Tactic:
refine TensorProduct.AlgebraTensorModule.curry_injective ?_

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
hpure_tensor :
  ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
⊢ TensorProduct.AlgebraTensorModule.curry
      ((LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).compl₂ (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
          TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q) +
        (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)).flip.compl₂
            (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
          TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) =
    TensorProduct.AlgebraTensorModule.curry
      (LinearMap.compr₂ (QuadraticMap.polarBilin (QuadraticForm.baseChange A Q))
        (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q)))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
⊢ x * 0 = 0

Tactic:
by simp_rw [mul_def, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) =
    (-1) ^ (j₂ * i₂ + (j₁ * i₁ + i₁ * j₂)) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)

Tactic:
mul_comm i₁ j₂

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) =
    (-1) ^ (j₂ * i₂ + (j₁ * i₁ + j₂ * i₁)) •
      ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂) ⊗ₜ[R] ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (GradedAlgebra.ι R M) m * (GradedAlgebra.ι R M) m = 0

Tactic:
GradedAlgebra.ι_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) 1) ⟨(ι R) m, ⋯⟩ * (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) 1) ⟨(ι R) m, ⋯⟩ = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd) = ⊤

Tactic:
rw [Submodule.eq_top_iff']
  intro x
  induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
  | zero => exact Submodule.zero_mem _
  | add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
  | homogeneous hm =>
    let ⟨m, hm⟩ := hm
    apply Set.mem_of_mem_of_subset hm
    rw [← ιMulti_span_fixedDegree]
    refine Submodule.span_mono fun _ hx ↦ ?_
    obtain ⟨y, rfl⟩ := hx
    exact ⟨⟨_, y⟩, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case coe
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
c : n
hc : l i = ↑c
⊢ ↑c = ⊤ ↔ A i = 0

Tactic:
simpa using fun h0 => (hA.isPivotEntry i).2 c hc (congrFun h0 c)

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
hlt : n < Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Tactic:
simp [hlt]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ ↑A 0 0 % ↑A 1 0 < |↑A 1 0|

Tactic:
exact Int.emod_lt_abs (A.1 0 0) h

Goal state after: