harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mem_rat_span_latticeBasis (x : K) :
    mixedEmbedding K x ∈ Submodule.span ℚ (Set.range (latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
simp_rw [map_rat_smul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), ((integralBasis K).repr x) x_1 • (mixedEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), ((integralBasis K).repr x) x_1 • (mixedEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
refine Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (mixedEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
rw [← Basis.sum_repr (integralBasis K) x, map_sum]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)

Tactic:
exact Set.mem_range_self i

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (mixedEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Tactic:
rw [← latticeBasis_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)
-- Mathlib/Data/Finite/Card.lean
theorem card_lt_card (ht : t.Finite) (hsub : s ⊂ t) : Nat.card s < Nat.card t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Fintype.card ↑s < Fintype.card ↑t

Tactic:
exact Set.card_lt_card hsub

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
have : Fintype t := Finite.fintype ht

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype ↑t
⊢ Nat.card ↑s < Nat.card ↑t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype ↑t
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Nat.card ↑s < Nat.card ↑t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
simp only [Nat.card_eq_fintype_card]

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Fintype.card ↑s < Fintype.card ↑t
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem factorial_mul_dpow_eq_pow {n : ℕ} (ha : a ∈ I) :
    (n ! : A) * hI.dpow n a = a ^ n

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ ↑n ! * hI.dpow n a = a ^ n

Tactic:
induction n with
| zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
| succ n ih =>
  rw [factorial_succ, mul_comm (n + 1)]
  nth_rewrite 1 [← (n + 1).choose_one_right]
  rw [← choose_symm_add, cast_mul, mul_assoc,
    ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

Result:
no goals

Proof state:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1)) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
nth_rewrite 1 [← (n + 1).choose_one_right]

Result:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1).choose 1) * hI.dpow (n + 1) a = a ^ (n + 1)

Proof state:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1).choose 1) * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
rw [← choose_symm_add, cast_mul, mul_assoc,
  ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

Result:
no goals

Proof state:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n + 1)! * hI.dpow (n + 1) a = a ^ (n + 1)

Tactic:
rw [factorial_succ, mul_comm (n + 1)]

Result:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑(n ! * (n + 1)) * hI.dpow (n + 1) a = a ^ (n + 1)

Proof state:
case zero
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
⊢ ↑0! * hI.dpow 0 a = a ^ 0

Tactic:
rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma liftAux_map {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow)
    (h : G.obj W ⟶ i.Y) (w : h ≫ i.f = G.map g ≫ f) :
    liftAux hF α s f ≫ F.map g.op = s.ι i ≫ R.map h.op ≫ α.app _ :=
  (Multifork.IsLimit.fac
    (hF.isLimitMultifork ⟨_, G.cover_lift J K (K.pullback_stable f S.2)⟩) _ _
      ⟨W, g, by simpa only [Sieve.functorPullback_apply, functorPullback_mem,
        Sieve.pullback_apply, ← w] using S.1.downward_closed i.hf h⟩).trans (by
        dsimp
        simp only [← Category.assoc]
        congr 1
        let r : S.Relation :=
          GrothendieckTopology.Cover.Relation.mk
            { f := G.map g ≫ f
              hf

Proof state:
case e_a
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op

Tactic:
let r : S.Relation :=
  GrothendieckTopology.Cover.Relation.mk
    { f := G.map g ≫ f
      hf := by simpa only [← w] using S.1.downward_closed i.hf h } i
    { g₁ := 𝟙 _
      g₂ := h
      w := by simpa using w.symm }

Result:
case e_a
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
r : S.Relation :=
  { fst := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }, snd := i,
    r :=
      { Z := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }.Y, g₁ := 𝟙 { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }.Y,
        g₂ := h, w := ⋯ } }
⊢ s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op
-- Mathlib/Order/Filter/Tendsto.lean
theorem Tendsto.of_neBot_imp {f : α → β} {la : Filter α} {lb : Filter β}
    (h : NeBot la → Tendsto f la lb) : Tendsto f la lb

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
lb : Filter β
h : ⊥.NeBot → Tendsto f ⊥ lb
⊢ Tendsto f ⊥ lb

Tactic:
exact tendsto_bot

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
⊢ Tendsto f la lb

Tactic:
rcases eq_or_neBot la with rfl | hla

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
lb : Filter β
h : ⊥.NeBot → Tendsto f ⊥ lb
⊢ Tendsto f ⊥ lb

case inr
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
hla : la.NeBot
⊢ Tendsto f la lb

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
hla : la.NeBot
⊢ Tendsto f la lb

Tactic:
exact h hla

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem eq_false_of_find?_eq_none {p : Fin n → Bool} (h : find? p = none) (i) : p i = false

Proof state:
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
hi : Option.guard (fun i => p i = true) i = none
⊢ p i = false

Tactic:
simp only [Option.guard] at hi

Result:
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
hi : (if p i = true then some i else none) = none
⊢ p i = false

Proof state:
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
⊢ p i = false

Tactic:
have hi := eq_none_of_findSome?_eq_none h i

Result:
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
hi : Option.guard (fun i => p i = true) i = none
⊢ p i = false

Proof state:
case isTrue
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
h✝ : p i = true
hi : some i = none
⊢ p i = false

Tactic:
contradiction

Result:
no goals

Proof state:
case isFalse
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
h✝ : ¬p i = true
hi : none = none
⊢ p i = false

Tactic:
simp [*]

Result:
no goals

Proof state:
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
hi : (if p i = true then some i else none) = none
⊢ p i = false

Tactic:
split at hi

Result:
case isTrue
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
h✝ : p i = true
hi : some i = none
⊢ p i = false

case isFalse
n : Nat
p : Fin n → Bool
h : find? p = none
i : Fin n
h✝ : ¬p i = true
hi : none = none
⊢ p i = false
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_le_div {n : ℕ} (pos : 0 < n) (np : ¬Prime n) : minFac n ≤ n / minFac n :=
  match minFac_dvd n with
  | ⟨0, h0⟩ => absurd pos <| by rw [h0, mul_zero]; decide
  | ⟨1, h1⟩ => by
    rw [mul_one] at h1
    rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
      not_le] at np
    rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
  | ⟨x + 2, hx⟩ => by
    conv_rhs =>
      congr
      rw [hx]
    rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
    exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac

Tactic:
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]

Result:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ x + 2

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < 0

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]

Result:
no goals

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n = (x + 2) * n.minFac

Tactic:
rwa [mul_comm]

Result:
no goals

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < n

Tactic:
rw [h0, mul_zero]

Result:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < 0

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
  not_le] at np

Result:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ x + 2

Tactic:
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩

Result:
no goals

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n.minFac ≤ n / n.minFac

Tactic:
rw [mul_one] at h1

Result:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Proof state:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n / n.minFac

Tactic:
conv_rhs =>
  congr
  rw [hx]

Result:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac
-- Mathlib/Topology/Algebra/Constructions.lean
@[to_additive] lemma topology_eq_inf :
    instTopologicalSpaceUnits =
      .induced (val : Mˣ → M) ‹_› ⊓ .induced (fun u ↦ ↑u⁻¹ : Mˣ → M) ‹_›

Proof state:
M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝¹ ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝¹ =
    TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝¹

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝¹

Tactic:
simp only [isInducing_embedProduct.1, instTopologicalSpaceProd, induced_inf,
  instTopologicalSpaceMulOpposite, induced_compose]

Result:
M : Type u_1
inst✝¹ : TopologicalSpace M
inst✝ : Monoid M
⊢ TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝¹ ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝¹ =
    TopologicalSpace.induced val inst✝¹ ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝¹
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_eq_zero_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    coverMincard T F U n = 0 ↔ F = ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅

Tactic:
refine Iff.intro (fun h ↦ subset_empty_iff.1 ?_) (fun F_empt ↦ by rw [F_empt, coverMincard_empty])

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
⊢ F ⊆ ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
F_empt : F = ∅
⊢ coverMincard T F U n = 0

Tactic:
rw [F_empt, coverMincard_empty]

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
⊢ F ⊆ ∅

Tactic:
have := coverMincard_finite_iff T F U n

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : coverMincard T F U n < ⊤ ↔ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n
⊢ F ⊆ ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : coverMincard T F U n < ⊤ ↔ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n
⊢ F ⊆ ∅

Tactic:
rw [h, eq_true ENat.top_pos, true_iff] at this

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = 0
⊢ F ⊆ ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = 0
⊢ F ⊆ ∅

Tactic:
simp only [IsDynCoverOf, Finset.mem_coe, Nat.cast_eq_zero, Finset.card_eq_zero, exists_eq_right,
  Finset.not_mem_empty, iUnion_of_empty, iUnion_empty] at this

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : F ⊆ ∅
⊢ F ⊆ ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : coverMincard T F U n = 0
this : F ⊆ ∅
⊢ F ⊆ ∅

Tactic:
exact this

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)]
lemma antivaryOn_inv_left : AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

Tactic:
simp [MonovaryOn, AntivaryOn]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
/-- If a family is complete orthogonal, it consists of idempotents. -/
lemma CompleteOrthogonalIdempotents.iff_ortho_complete :
    CompleteOrthogonalIdempotents e ↔ Pairwise (e · * e · = 0) ∧ ∑ i, e i = 1

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ CompleteOrthogonalIdempotents e ↔ (Pairwise fun x1 x2 => e x1 * e x2 = 0) ∧ ∑ i : I, e i = 1

Tactic:
rw [completeOrthogonalIdempotents_iff, orthogonalIdempotents_iff, and_assoc, and_iff_right_of_imp]

Result:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ (Pairwise fun x1 x2 => e x1 * e x2 = 0) ∧ ∑ i : I, e i = 1 → ∀ (i : I), IsIdempotentElem (e i)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
⊢ (Pairwise fun x1 x2 => e x1 * e x2 = 0) ∧ ∑ i : I, e i = 1 → ∀ (i : I), IsIdempotentElem (e i)

Tactic:
intro ⟨ortho, complete⟩ i

Result:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
ortho : Pairwise fun x1 x2 => e x1 * e x2 = 0
complete : ∑ i : I, e i = 1
i : I
⊢ IsIdempotentElem (e i)
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (x : G) (n : ℕ) : f (x + n) = f x + n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℕ
⊢ f (x + ↑n) = f x + ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem mem_of_mem_equivPair_tail {i j : ι} {w : Word M} (m : M i) :
    (⟨i, m⟩ ∈ (equivPair j w).tail.toList) → ⟨i, m⟩ ∈ w.toList

Proof state:
case inl
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
h : ⟨i, m⟩ ∈ w.toList.tail
⊢ ⟨i, m⟩ ∈ w.toList

Tactic:
exact List.mem_of_mem_tail h

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ ⟨i, m⟩ ∈ ((equivPair j) w).tail.toList → ⟨i, m⟩ ∈ w.toList

Tactic:
rw [mem_equivPair_tail_iff]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ w.toList

Proof state:
case inr
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ w.toList

Tactic:
cases w.toList <;> simp (config := {contextual := true})

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ w.toList

Tactic:
rintro (h | h)

Result:
case inl
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
h : ⟨i, m⟩ ∈ w.toList.tail
⊢ ⟨i, m⟩ ∈ w.toList

case inr
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
h : i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈ w.toList

Proof state:
case inr
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
h : i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈ w.toList

Tactic:
revert h

Result:
case inr
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ w.toList
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem ext {f g : M ≃ₚ[L] N} (h_dom : f.dom = g.dom) : (∀ x : M, ∀ h : x ∈ f.dom,
    subtype _ (f.toEquiv ⟨x, h⟩) = subtype _ (g.toEquiv ⟨x, (h_dom ▸ h)⟩)) → f = g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_dom : f.dom = g.dom
⊢ (∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) → f = g

Tactic:
intro h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_dom : f.dom = g.dom
h : ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g

Proof state:
case h.h.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
x : M
hx : x ∈ g.dom
⊢ ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion ⋯)))
      ⟨x, hx⟩ =
    (g.cod.subtype.comp g.toEquiv.toEmbedding) ⟨x, hx⟩

Tactic:
exact h x hx

Result:
no goals

Proof state:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = g.dom
h :
  ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
cases h_dom

Result:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_inv_eq_self (f : G → E) (μ : Measure G) [IsInvInvariant μ] :
    ∫ x, f x⁻¹ ∂μ = ∫ x, f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
h : MeasurableEmbedding fun x => x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ

Tactic:
rw [← h.integral_map, map_inv_eq_self]

Result:
no goals

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ

Tactic:
have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding

Result:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
h : MeasurableEmbedding fun x => x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ