mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Icc (natAdd ?m i) (natAdd ?m j) = Icc (natAdd m i) (natAdd m j)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Icc (natAdd m i) (natAdd m j) = Icc (natAdd m i) (natAdd m j)

n m : ℕ
i j : Fin n
⊢ Icc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ico (natAdd ?m i) (natAdd ?m j) = Ico (natAdd m i) (natAdd m j)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) = Ico (natAdd m i) (natAdd m j)

n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ioc (natAdd ?m i) (natAdd ?m j) = Ioc (natAdd m i) (natAdd m j)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) = Ioc (natAdd m i) (natAdd m j)

n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ioo (natAdd ?m i) (natAdd ?m j) = Ioo (natAdd m i) (natAdd m j)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) = Ioo (natAdd m i) (natAdd m j)

n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioo i j = Ioo (natAdd m i) (natAdd m j)

Tactic:
by
  rw [← preimage_natAdd_Ioo_natAdd, image_preimage_eq_of_subset]
  exact Ioo_subset_Ioi_self.trans <| image_natAdd_Ioi m i ▸ image_subset_range _ _

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ici (i.addNat ?m) = Ici (i.addNat m)

pp: case m
n m : ℕ
i : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) = Ici (i.addNat m)

n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ioi (i.addNat ?m) = Ioi (i.addNat m)

pp: case m
n m : ℕ
i : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) = Ioi (i.addNat m)

n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Icc (i.addNat ?m) (j.addNat ?m) = Icc (i.addNat m) (j.addNat m)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) = Icc (i.addNat m) (j.addNat m)

n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case hs
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∃ i ∈ hf.toFinset, 1 < f i

Tactic:
· aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ico (i.addNat ?m) (j.addNat ?m) = Ico (i.addNat m) (j.addNat m)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) = Ico (i.addNat m) (j.addNat m)

n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ioc (i.addNat ?m) (j.addNat ?m) = Ioc (i.addNat m) (j.addNat m)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) = Ioc (i.addNat m) (j.addNat m)

n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ioo (i.addNat ?m) (j.addNat ?m) = Ioo (i.addNat m) (j.addNat m)

pp: case m
n m : ℕ
i j : Fin n
⊢ ℕ

Tactic:
image_preimage_eq_of_subset

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) = Ioo (i.addNat m) (j.addNat m)

n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (linearCombination R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x

Tactic:
simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∑ a ∈ s with f a ≠ 0, f a • g a = ∑ a ∈ s, f a • g a
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iio i ↔ x✝ ∈ Ioi i.rev

Tactic:
simp [rev_lt_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)) ⟨b i, h⟩ = b i

Tactic:
reindex_apply,

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexRange (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
x : α
⊢ f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1

Tactic:
contrapose!

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ : α → M
r : S
v : α → M
⊢ Fintype.linearCombination R (r • v) = (RingHom.id S) r • Fintype.linearCombination R v

Tactic:
ext; simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b')) (b' i') = LinearMap.id (b i)

Tactic:
b'.constr_basis,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ (g ∘ ⇑b') i' = LinearMap.id (b i)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ g (b' i') = LinearMap.id (b i)

Tactic:
hi',

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ g (f (b i)) = LinearMap.id (b i)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b)) (((b'.constr R) (g ∘ ⇑b')) (b' i)) = LinearMap.id (b' i)

Tactic:
b'.constr_basis,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b)) ((g ∘ ⇑b') i) = LinearMap.id (b' i)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ f (b i') = LinearMap.id (b' i)

Tactic:
hi',

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ f (g (b' i)) = LinearMap.id (b' i)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}

Tactic:
by
  rw [range_cons, range_cons_empty, Set.singleton_union]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j

Tactic:
rw [← finprod_mem_univ f, ← finprod_mem_univ g]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ y ≠ 0

Tactic:
← y.cast_ne_zero (R := ℕ∞)

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ ↑y ≠ 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

Tactic:
simp only [one_epow, le_refl]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndependent R (⇑f ∘ v)
⊢ LinearIndependent R v

Tactic:
rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v))
⊢ LinearIndependent R v
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Icc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Icc a b, f (castAdd m i)

Tactic:
by
  simp [← map_castAddEmb_Icc]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i (i' x✝¹) = i (i' x✝)
⊢ x✝¹ = x✝

Tactic:
hi',

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : x✝¹ = i (i' x✝)
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i (i' x✝¹) = i (i' x✝)
⊢ x✝¹ = x✝

Tactic:
rwa [hi', hi'] at h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m

Tactic:
hc (i' r) m,

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ i (i' r) • j m = r • j m
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
partialProd_succ,

Goal state after:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * (partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) = f x.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i

Tactic:
partialProd_succ,

Goal state after:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * (partialProd f i.castSucc * f i) = f i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ

Tactic:
partialProd_succ,

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).succ

Tactic:
partialProd_succ,

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)